EVERY_LT : (list_tactic list -> list_tactic)
STRUCTURE
Tactical
SYNOPSIS
Sequentially applies all the list-tactics in a given list of list-tactics.
DESCRIPTION
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.
SEEALSO
THEN_LT
HOL  Kananaskis-13