A tactical like THEN that applies the second tactic only to the
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.
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.
THEN1 can be applied to make the proof more linear, avoiding
unnecessary THENLs. It is especially useful when used with
For example, given the goal
simple_goal /\ complicated_goal
(CONJ_TAC THEN1 T0)