----------------------------------------------------------------------
WEAKEN_CONSEQ_CONV_RULE                                   (ConseqConv)
----------------------------------------------------------------------
WEAKEN_CONSEQ_CONV_RULE : (directed_conseq_conv -> thm -> thm)

SYNOPSIS
Tries to weaken the conclusion of a theorem consisting of an
implication.

DESCRIBE
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}.

SEEALSO
ConseqConv.STRENGTHEN_CONSEQ_CONV_RULE.

----------------------------------------------------------------------