EVERY_LTTactical.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 LTnIf the list-tactic list is empty, the resulting list-tactic has no effect.
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.
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.