If c is a conversion, then CONV_RULE c is an inference rule that applies
c to the conclusion of a theorem. That is, if c maps a term `t` to the
theorem |- t = t', then the rule CONV_RULE c infers |- t' from the
theorem |- t. More precisely, if c `t` returns A' |- t = t', then:
A |- t
-------------- CONV_RULE c
A u A' |- t'
Note that if the conversion c returns a theorem with assumptions,
then the resulting inference rule adds these to the assumptions of the
theorem it returns.
FAILURE CONDITIONS
CONV_RULE c th fails if c fails when applied to the conclusion of th. The
function returned by CONV_RULE c will also fail if the ML function c is
not, in fact, a conversion (i.e. a function that maps a term t to a theorem
|- t = t').
EXAMPLE
# CONV_RULE BETA_CONV (ASSUME `(\x. x < 2) 1`);;
val it : thm = (\x. x < 2) 1 |- 1 < 2