----------------------------------------------------------------------
THEN                                                        (Tactical)
----------------------------------------------------------------------
op THEN : tactic * tactic -> tactic}
op THEN : list_tactic * tactic -> list_tactic

SYNOPSIS
Applies a tactic to all subgoals produced by a tactic or list-tactic.

KEYWORDS
tactical.

DESCRIBE
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:

   EQ_TAC THENL [ASM_REWRITE_TAC[], ASM_REWRITE_TAC[]]

can be replaced by the briefer:

   EQ_TAC THEN ASM_REWRITE_TAC[]




SEEALSO
Tactical.EVERY, Tactical.ORELSE, Tactical.THENL, Tactical.THEN_LT.

----------------------------------------------------------------------