THEN1

op Tactical.THEN1 : tactic * tactic -> tactic

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

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]

See also

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