----------------------------------------------------------------------
REVERSE                                                     (Tactical)
----------------------------------------------------------------------
REVERSE : (tactic -> tactic)

SYNOPSIS
Reverses the order of the generated subgoals.

KEYWORDS
tactical.

DESCRIBE
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
Tactical.EVERY, Tactical.FIRST, Tactical.ORELSE, Tactical.THEN,
Tactical.THEN1, Tactical.THENL.

----------------------------------------------------------------------