\DOC

\TYPE {QCONV : conv -> conv}

\SYNOPSIS Stops a conversion raising the {UNCHANGED} exception.

\KEYWORDS
conversion.

\DESCRIBE
If conversion {c} applied to term {t} raises the {UNCHANGED}
exception, then {QCONV c t} instead returns the theorem {|- t = t}.

\FAILURE
{QCONV c t} fails if the application of {c} to {t} fails.

\SEEALSO
Conv.UNCHANGED, Conv.CHANGED_CONV, Conv.QCHANGED_CONV.

\ENDDOC