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