REFL_CONSEQ_CONV : conseq_conv
STRUCTURE
LIBRARY
ConseqConv
SYNOPSIS
Given a term t of type bool this consequence conversion returns the theorem |- t ==> t.
SEEALSO
HOL  Trindemossen-1