EVERY : (tactic list -> tactic)

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

- 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

HOL Kananaskis-13