TRUE_CONSEQ_CONV

ConseqConv.TRUE_CONSEQ_CONV : conseq_conv

Given a term t of type bool this consequence conversion returns the theorem |- t ==> T.

See also

ConseqConv.FALSE_CONSEQ_CONV, ConseqConv.REFL_CONSEQ_CONV, ConseqConv.TRUE_FALSE_REFL_CONSEQ_CONV