EVERYTactical.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:
EVERY [T1;...;Tn] = T1 THEN ... THEN TnIf the tactic list is empty, the resulting tactic has no effect.
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.