op ORELSE : tactic * tactic -> tactic
STRUCTURE
Tactical
SYNOPSIS
Applies first tactic, and if it fails, applies the second instead.
DESCRIPTION
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
EVERY
,
FIRST
,
THEN
HOL
Kananaskis-13