1\DOC QCHANGED_CONV
2
3\TYPE {QCHANGED_CONV : conv -> conv}
4
5\SYNOPSIS
6Makes a conversion fail if applying it raises the {UNCHANGED} exception.
7
8\KEYWORDS
9conversional.
10
11\DESCRIBE
12If {c} is a conversion that maps a term {t} to a theorem {|- t = t'},
13then so too is {QCHANGED_CONV c}.  If {c} applied to {t} raises the
14special {UNCHANGED} exception used by conversions to indicate that
15they haven't changed an input, then {QCHANGED_CONV c} will fail,
16raising a different exception {HOL_ERR ...} when applied to {t}.
17
18The purpose of this is that some enclosing functions handle the 
19{UNCHANGED} exception as though {c} had succeeded by returning
20the theorem {|- t = t}.
21
22This behaviour is similar to that of {CHANGED_CONV}, except that that
23conversion also fails if the conversion {c} returns a theorem when
24applied to {t}, and if that theorem has alpha-convertible left and
25right hand sides.
26
27\FAILURE
28{QCHANGED_CONV c t} fails (other than by raising {UNCHANGED})
29if {c} applied {t} raises the {UNCHANGED} exception,
30or if {c} fails otherwise when applied to {t}.
31
32\USES
33{QCHANGED_CONV} can be used in places where {CHANGED_CONV} is
34appropriate, and where one knows that the conversion argument will not
35return an instance of reflexivity, or if one does not mind this
36occurring and not being trapped.  Because it is no more than an
37exception handler, {QCHANGED_CONV} is very efficient.
38
39\SEEALSO
40Conv.UNCHANGED, Conv.CHANGED_CONV.
41
42\ENDDOC
43