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