op THEN1 : tactic * tactic -> tactic
STRUCTURE
Tactical
SYNOPSIS
A tactical like THEN that applies the second tactic only to the first subgoal.
DESCRIPTION
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 THENLs. 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
EVERY, ORELSE, REVERSE, THEN, THENL
HOL  Kananaskis-13