----------------------------------------------------------------------
ORELSE_LT                                                   (Tactical)
----------------------------------------------------------------------
op ORELSE_LT : list_tactic * list_tactic -> list_tactic

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

KEYWORDS
tactical.

DESCRIBE
If {ltac1} and {ltac2} are list-tactics, {ltac1 ORELSE_LT ltac2}
is a list-tactic which applies {ltac1} to a goal list, and if it fails,
applies {ltac2} to the goals.

FAILURE
The application of {ORELSE_LT} to a pair of list-tactics never fails.
The resulting list-tactic fails if both {ltac1} and {ltac2} fail
when applied to the relevant goals.

SEEALSO
Tactical.ORELSE, Tactical.THEN_LT.

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