UNCHANGED : exception
STRUCTURE
SYNOPSIS
Raised by a conversion to indicate that a term should remain unchanged.
DESCRIPTION
When a conversion c is applied to a term t this can raise the exception UNCHANGED to indicate that t should not be changed to another term t'.

Since in this case we have a function raising an exception, we describe this as failure of the function c. However it may be the intended result (as used, for example, by ALL_CONV or TRY_CONV).

When conversions are combined using THENC or ORELSEC, raising UNCHANGED is treated as though |- t = t were returned.

When a conversion c is used to produce an inference rule CONV_RULE c or a tactic CONV_TAC c, and c raises UNCHANGED, the rule CONV_RULE c or tactic CONV_TAC c succeeds, returning the theorem or goal unchanged.

SEEALSO
HOL  Kananaskis-13