CHANGED_TAC : (tactic -> tactic)
STRUCTURE
Tactical
SYNOPSIS
Makes a tactic fail if it has no effect.
DESCRIPTION
When applied to a tactic
T
, the tactical
CHANGED_TAC
gives a new tactic which is the same as
T
if that has any effect, and otherwise fails.
FAILURE
The application of
CHANGED_TAC
to a tactic never fails. The resulting tactic fails if the basic tactic either fails or has no effect.
SEEALSO
TRY
,
VALID
HOL
Kananaskis-14