\DOC CHANGED_CONV

\TYPE {CHANGED_CONV : (conv -> conv)}

\SYNOPSIS
Makes a conversion fail if applying it leaves a term unchanged.

\KEYWORDS
conversional.

\DESCRIBE
If {c} is a conversion that maps a term {``t``} to a theorem {|- t = t'},
where {t'} is alpha-equivalent to {t}, or if {c} raises the
{UNCHANGED} exception when applied to {``t``}, then {CHANGED_CONV c}
is a conversion that fails when applied to the term {``t``}. If {c}
maps {``t``} to {|- t = t'}, where {t'} is not alpha-equivalent to
{t}, then {CHANGED_CONV c} also maps {``t``} to {|- t = t'}. That is,
{CHANGED_CONV c} is the conversion that behaves exactly like {c},
except that it fails whenever the conversion {c} would leave its input
term unchanged (up to alpha-equivalence).

When {CHANGED_CONV c t} fails, it raises an exception {HOL_ERR ...},
not {UNCHANGED}, since some enclosing functions handle the 
{UNCHANGED} exception as though {c} had succeeded by returning
the theorem {|- t = t}.

\FAILURE
{CHANGED_CONV c ``t``} fails if {c} maps {``t``} to {|- t = t'}, where
{t'} is alpha-equivalent to {t}, or if {c} raises the {UNCHANGED}
exception when applied to {``t``}, or if {c} fails when applied to
{``t``}.  The function returned by {CHANGED_CONV c} may also fail if
the ML function {c:term->thm} is not, in fact, a conversion (i.e. a
function that maps a term {t} to a theorem {|- t = t'}).

\USES
{CHANGED_CONV} is used to transform a conversion that may leave terms
unchanged, and therefore may cause a nonterminating computation if
repeated, into one that can safely be repeated until application of it
fails to substantially modify its input term.

\SEEALSO
Conv.UNCHANGED, Conv.QCHANGED_CONV.

\ENDDOC