WEAKEN_CONSEQ_CONV_RULEConseqConv.WEAKEN_CONSEQ_CONV_RULE : (directed_conseq_conv -> thm -> thm)Tries to weaken the conclusion of a theorem consisting of an implication.
Given a theorem of the form |- A ==> C and a directed
consequence conversion c a call of
WEAKEN_CONSEQ_CONV_RULE c thm tries to weaken
C to a predicate wC using c. If
it succeeds it returns the theorem |- A ==> wC.