----------------------------------------------------------------------
conseq_conv                                               (ConseqConv)
----------------------------------------------------------------------
type conseq_conv

SYNOPSIS
A type for functions that given a term produce a theorem with
an implication at the top level.

DESCRIBE
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


EXAMPLE
Examples of simple consequence conversion are {TRUE_CONSEQ_CONV} and
{FALSE_CONSEQ_CONV}.

SEEALSO
ConseqConv.directed_conseq_conv,
ConseqConv.TRUE_FALSE_REFL_CONSEQ_CONV.

----------------------------------------------------------------------