REVERSE : (tactic -> tactic)
STRUCTURE
Tactical
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 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.
SEEALSO
EVERY, FIRST, ORELSE, THEN, THEN1, THENL
HOL  Kananaskis-13