op ORELSE_LT : list_tactic * list_tactic -> list_tactic
STRUCTURE
SYNOPSIS
Applies first list-tactic, and if it fails, applies the second instead.
DESCRIPTION
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
HOL  Trindemossen-1