REFL_CONSEQ_CONV

ConseqConv.REFL_CONSEQ_CONV : conseq_conv

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

See also

ConseqConv.TRUE_CONSEQ_CONV, ConseqConv.FALSE_CONSEQ_CONV, ConseqConv.TRUE_FALSE_REFL_CONSEQ_CONV