EVERY : tactic list -> tactic
Sequentially applies all the tactics in a given list of tactics.
When applied to a list of tactics [t1; ... ;tn], and a goal g, the tactical
EVERY applies each tactic in sequence to every
subgoal generated by the previous one. This can be represented as:
If the tactic list is empty, the resulting tactic has no effect.
EVERY [t1;...;tn] = t1 THEN ... THEN tn
- FAILURE CONDITIONS
The application of EVERY to a tactic list never fails. The resulting
tactic fails iff any of the component tactics do.
It is possible to use EVERY instead of THEN, but probably
stylistically inferior. EVERY is more useful when applied to a list of
tactics generated by a function.
- SEE ALSO
FIRST, MAP_EVERY, THEN.