----------------------------------------------------------------------
CHANGED_TAC                                                 (Tactical)
----------------------------------------------------------------------
CHANGED_TAC : (tactic -> tactic)

SYNOPSIS
Makes a tactic fail if it has no effect.

KEYWORDS
tactical.

DESCRIBE
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
Tactical.TRY, Tactical.VALID.

----------------------------------------------------------------------