----------------------------------------------------------------------
QCONV                                                           (Conv)
----------------------------------------------------------------------
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.

----------------------------------------------------------------------