1\DOC TRY_CONV 2 3\TYPE {TRY_CONV : conv -> conv} 4 5\SYNOPSIS 6Attempts to apply a conversion; 7applies identity conversion in case of failure. 8 9\KEYWORDS 10conversion, failure, unchanged. 11 12\DESCRIBE 13 14{TRY_CONV c t} attempts to apply the conversion {c} to the term {t}; 15if this fails, then the identity conversion is applied instead. That 16is, if {c} is a conversion that maps a term {t} to the theorem {|- t = t'}, 17then the conversion {TRY_CONV c} also maps {t} to {|- t = t'}. But if {c} 18fails when applied to {t}, then {TRY_CONV c t} raises the {UNCHANGED} 19exception (which is understood to mean the instance of reflexivity, 20{|- t = t}). If {c} applied to {t} raises the {UNCHANGED} exception, 21then so too does {TRY_CONV c t}. 22 23\FAILURE 24Never fails, except that the {UNCHANGED} exception can be raised. 25 26\SEEALSO 27Conv.UNCHANGED, Conv.QCHANGED_CONV, Conv.ALL_CONV, Conv.QCONV. 28\ENDDOC 29