Classical conversions (see Conv) convert a given term t to a term
eqt that is equal to t. For a boolean term t, it is however
sometimes useful not to preserve equivalence, but to either strengthen
t to st or to weaken it to wt. The type conseq_conv is used
for ML functions that perform these operations. These ML Functions are
called consequence conversions in the following.
Given a consequence conversion CONSEQ_CONV and a term t, then
CONSEQ_CONV can either fail with an HOL_ERR-exception,
raise an UNCHANGED-exception or produce a theorem of one of the
following forms:
1. st ==> t
2. t ==> wt
3. t = eqt