1\DOC UNCHANGED 2 3\TYPE {UNCHANGED : exception} 4 5\SYNOPSIS 6Raised by a conversion to indicate that a term should remain unchanged. 7 8\KEYWORDS 9conversion, unchanged, failure. 10 11\DESCRIBE 12When a conversion {c} is applied to a term {t} this can raise the 13exception {UNCHANGED} to indicate that {t} should not be changed 14to another term {t'}. 15 16Since in this case we have a function raising an exception, 17we describe this as failure of the function {c}. 18However it may be the intended result (as used, for example, 19by {ALL_CONV} or {TRY_CONV}). 20 21When conversions are combined using {THENC} or {ORELSEC}, 22raising {UNCHANGED} is treated as though {|- t = t} were returned. 23 24When a conversion {c} is used to produce an inference rule {CONV_RULE c} 25or a tactic {CONV_TAC c}, and {c} raises {UNCHANGED}, 26the rule {CONV_RULE c} or tactic {CONV_TAC c} succeeds, 27returning the theorem or goal unchanged. 28 29\SEEALSO 30Abbrev.conv, Conv.QCONV, Conv.QCHANGED_CONV, 31Conv.ALL_CONV, Conv.TRY_CONV, Conv.CONV_RULE, 32Tactic.CONV_TAC, Conv.THENC, Conv.ORELSEC. 33\ENDDOC 34