CHANGED_TAC : tactic -> tactic
Makes a tactic fail if it has no effect.
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.
Occasionally useful in controlling complicated tactic compositions. Also
sometimes convenient just to check that a step did indeed modify a goal.
- SEE ALSO