TRY : (tactic -> tactic)
STRUCTURE
Tactical
SYNOPSIS
Makes a tactic have no effect rather than fail.
DESCRIPTION
For any tactic
T
, the application
TRY T
gives a new tactic which has the same effect as
T
if that succeeds, and otherwise has no effect.
FAILURE
The application of
TRY
to a tactic never fails. The resulting tactic never fails.
SEEALSO
CHANGED_TAC
,
VALID
HOL
Kananaskis-14