STRENGTHEN_CONSEQ_CONV_RULE : directed_conseq_conv -> thm -> thm
STRUCTURE
SYNOPSIS
Tries to strengthen the antecedent of a theorem consisting of an implication.
DESCRIPTION
Given a theorem of the form |- A ==> C and a directed consequence conversion c a call of STRENGTHEN_CONSEQ_CONV_RULE c thm tries to strengthen A to a predicate sA using c. If it succeeds it returns the theorem |- sA ==> C.
SEEALSO
HOL  Kananaskis-10