EVERY_LT
Tactical.EVERY_LT : (list_tactic list -> list_tactic)
Sequentially applies all the list-tactics in a given list of list-tactics.
When applied to a list of list-tactics [LT1; ... ;LTn], and a goal
g, the tactical EVERY_LT applies each list-tactic in sequence to
every subgoal generated by the previous one. This can be represented as:
EVERY_LT [LT1;...;LTn] = LT1 THEN_LT ... THEN_LT LTn
If the list-tactic list is empty, the resulting list-tactic has no effect.
Failure
The application of EVERY_LT to a list-tactic list never fails. The
resulting list-tactic fails iff any of the component list-tactics do.
Comments
It is possible to use EVERY_LT instead of THEN_LT, but probably
stylistically inferior. EVERY_LT is more useful when applied to a list
of list-tactics generated by a function.