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