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