op THEN : tactic * tactic -> tactic} op THEN : list_tactic * tactic -> list_tactic

- STRUCTURE
- SYNOPSIS
- Applies a tactic to all subgoals produced by a tactic or list-tactic.
- DESCRIPTION
- If T1 and T2 are tactics, T1 THEN T2 is a tactic which applies T1 to a goal, then applies the tactic T2 to all the subgoals generated. If T1 solves the goal then T2 is never applied.
Alternatively, T1 may be a list-tactic which is applied to an initial list of goals.

- FAILURE
- The application of THEN to a pair of tactics never fails. The resulting tactic fails if T1 fails when applied to the goal, or if T2 does when applied to any of the resulting subgoals.
- COMMENTS
- Although normally used to sequence tactics which generate a single subgoal, it is worth remembering that it is sometimes useful to apply the same tactic to multiple subgoals; sequences like the following:can be replaced by the briefer:
EQ_TAC THENL [ASM_REWRITE_TAC[], ASM_REWRITE_TAC[]]

EQ_TAC THEN ASM_REWRITE_TAC[]

- SEEALSO

HOL Kananaskis-13