1\DOC
2
3\TYPE {QCONV : conv -> conv}
4
5\SYNOPSIS Stops a conversion raising the {UNCHANGED} exception.
6
7\KEYWORDS
8conversion.
9
10\DESCRIBE
11If conversion {c} applied to term {t} raises the {UNCHANGED}
12exception, then {QCONV c t} instead returns the theorem {|- t = t}.
13
14\FAILURE
15{QCONV c t} fails if the application of {c} to {t} fails.
16
17\SEEALSO
18Conv.UNCHANGED, Conv.CHANGED_CONV, Conv.QCHANGED_CONV.
19
20\ENDDOC
21