op THEN1 : tactic * tactic -> tactic

- STRUCTURE
- 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 goalthe tactic
simple_goal /\ complicated_goal

avoids the extra indentation of(CONJ_TAC THEN1 T0) THEN T1 THEN T2 THEN ... THEN Tn

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

- SEEALSO

HOL Kananaskis-13