----------------------------------------------------------------------
THEN1                                                       (Tactical)
----------------------------------------------------------------------
op THEN1 : tactic * tactic -> tactic

SYNOPSIS
A tactical like {THEN} that applies the second tactic only to the
first subgoal.

KEYWORDS
tactical.

DESCRIBE
If {T1} and {T2} are tactics, {T1 THEN1 T2} is a tactic which applies
{T1} to a goal, then applies the tactic {T2} to the first subgoal
generated. {T1} must produce at least one subgoal, and {T2} must
completely solve the first subgoal of {T1}.

FAILURE
The application of {THEN1} to a pair of tactics never fails.  The
resulting tactic fails if {T1} fails when applied to the goal, if {T1}
does not produce at least one subgoal (i.e., {T1} completely solves
the goal), or if {T2} does not completely solve the first subgoal
generated by {T1}.

COMMENTS
{THEN1} can be applied to make the proof more linear, avoiding
unnecessary {THENL}s. It is especially useful when used with
{REVERSE}.

EXAMPLE
For example, given the goal

   simple_goal /\ complicated_goal

the tactic

   (CONJ_TAC THEN1 T0)
   THEN T1
   THEN T2
   THEN ...
   THEN Tn

avoids the extra indentation of

   CONJ_TAC THENL
   [T0,
    T1
    THEN T2
    THEN ...
    THEN Tn]




SEEALSO
Tactical.EVERY, Tactical.ORELSE, Tactical.REVERSE, Tactical.THEN,
Tactical.THENL.

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