CHANGED_TAC : tactic -> tactic
- 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 CONDITIONS
-
The application of CHANGED_TAC to a tactic never fails. The resulting
tactic fails if the basic tactic either fails or has no effect.
- USES
-
Occasionally useful in controlling complicated tactic compositions. Also
sometimes convenient just to check that a step did indeed modify a goal.
- SEE ALSO
-
TRY, VALID.