CHANGED_CONSEQ_CONV
ConseqConv.CHANGED_CONSEQ_CONV : (conseq_conv -> conseq_conv)
Makes a consequence conversion fail if applying it leaves a term unchanged.
If c is a consequence conversion that maps a term ``t`` to a
theorem |- t = t', |- t' ==> t or |- t ==> t', where t' is
alpha-equivalent to t, or if c raises the UNCHANGED exception when
applied to ``t``, then CHANGED_CONSEQ_CONV c fails when
applied to the term ``t``. Otherwise, CHANGED_CONSEQ_CONV c
behaves like c.