QCONV : conv -> conv
STRUCTURE
SYNOPSIS
Stops a conversion raising the UNCHANGED exception.
DESCRIPTION
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
HOL  Kananaskis-14