REVERSE
Tactical.REVERSE : (tactic -> tactic)
Reverses the order of the generated subgoals.
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 goal
G1 /\ G2
use
CONJ_TAC THEN1 T0
THEN ...
if the first conjunct is easily dispatched with T0, and
REVERSE CONJ_TAC THEN1 T0
THEN ...
if it is the second conjunct that yields.
See also
Tactical.EVERY,
Tactical.FIRST,
Tactical.ORELSE,
Tactical.THEN, Tactical.THEN1,
Tactical.THENL