EVERY : (tactic list -> tactic)
STRUCTURE
Tactical
SYNOPSIS
Sequentially applies all the tactics in a given list of tactics.
DESCRIPTION
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 Tn
If the tactic list is empty, the resulting tactic has no effect.
FAILURE
The application of EVERY to a tactic list never fails. The resulting tactic fails iff any of the component tactics do.
COMMENTS
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.
SEEALSO
FIRST, MAP_EVERY, THEN
HOL  Kananaskis-13