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