TRY : (tactic -> tactic)
STRUCTURE
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
HOL  Trindemossen-1