QCHANGED_CONVConv.QCHANGED_CONV : conv -> convMakes a conversion fail if applying it raises the
UNCHANGED exception.
If c is a conversion that maps a term t to
a theorem |- t = t', then so too is
QCHANGED_CONV c. If c applied to
t raises the special UNCHANGED exception used
by conversions to indicate that they haven’t changed an input, then
QCHANGED_CONV c will fail, raising a different exception
HOL_ERR ... when applied to t.
The purpose of this is that some enclosing functions handle the
UNCHANGED exception as though c had succeeded
by returning the theorem |- t = t.
This behaviour is similar to that of CHANGED_CONV,
except that that conversion also fails if the conversion c
returns a theorem when applied to t, and if that theorem
has alpha-convertible left and right hand sides.
QCHANGED_CONV c t fails (other than by raising
UNCHANGED) if c applied t raises
the UNCHANGED exception, or if c fails
otherwise when applied to t.
QCHANGED_CONV can be used in places where
CHANGED_CONV is appropriate, and where one knows that the
conversion argument will not return an instance of reflexivity, or if
one does not mind this occurring and not being trapped. Because it is no
more than an exception handler, QCHANGED_CONV is very
efficient.