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