TRUE_FALSE_REFL_CONSEQ_CONV : directed_conseq_conv
STRUCTURE
ConseqConv
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
TRUE_CONSEQ_CONV
,
FALSE_CONSEQ_CONV
,
REFL_CONSEQ_CONV
HOL
Kananaskis-14