REVERSE : (tactic -> tactic)

- STRUCTURE
- SYNOPSIS
- Reverses the order of the generated subgoals.
- DESCRIPTION
- The tactic REVERSE T is a tactic which applies T to a goal, and reverses the order of the subgoals generated by T.
- FAILURE
- The application of REVERSE to a tactic T never fails. The resulting composite tactic REVERSE T fails when applied to a goal if and only if T fails.
- COMMENTS
- Intended for use with THEN1 to pick the ‘easy’ subgoal.
- EXAMPLE
- Given a goaluse
G1 /\ G2

if the first conjunct is easily dispatched with T0, andCONJ_TAC THEN1 T0 THEN ...

if it is the second conjunct that yields.REVERSE CONJ_TAC THEN1 T0 THEN ...

- SEEALSO

HOL Kananaskis-13