TRUE_FALSE_REFL_CONSEQ_CONV : directed_conseq_conv
STRUCTURE
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
HOL  Kananaskis-14