TRUE_CONSEQ_CONV : conseq_conv
STRUCTURE
ConseqConv
SYNOPSIS
Given a term
t
of type
bool
this consequence conversion returns the theorem
|- t ==> T
.
SEEALSO
FALSE_CONSEQ_CONV
,
REFL_CONSEQ_CONV
,
TRUE_FALSE_REFL_CONSEQ_CONV
HOL
Kananaskis-13