----------------------------------------------------------------------
TRUE_FALSE_REFL_CONSEQ_CONV                               (ConseqConv)
----------------------------------------------------------------------
TRUE_FALSE_REFL_CONSEQ_CONV : directed_conseq_conv

LIBRARY
ConseqConv

SYNOPSIS
Given a term {t} of type {bool} this directed consequence conversion
returns the theorem {|- F ==> t} for {CONSEQ_CONV_STRENGTHEN_direction},
the theorem {|- t ==> T} for {CONSEQ_CONV_WEAKEN_direction} and
{|- t = t} for {CONSEQ_CONV_UNKNOWN_direction}.

SEEALSO
ConseqConv.TRUE_CONSEQ_CONV, ConseqConv.FALSE_CONSEQ_CONV,
ConseqConv.REFL_CONSEQ_CONV.

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