----------------------------------------------------------------------
ORELSE                                                      (Tactical)
----------------------------------------------------------------------
op ORELSE : tactic * tactic -> tactic

SYNOPSIS
Applies first tactic, and if it fails, applies the second instead.

KEYWORDS
tactical.

DESCRIBE
If {T1} and {T2} are tactics, {T1 ORELSE T2} is a tactic which applies {T1} to
a goal, and if it fails, applies {T2} to the goal instead.

FAILURE
The application of {ORELSE} to a pair of tactics never fails.
The resulting tactic fails if both {T1} and {T2} fail when applied to the
relevant goal.

SEEALSO
Tactical.EVERY, Tactical.FIRST, Tactical.THEN.

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