THEN_CONSEQ_CONV
ConseqConv.THEN_CONSEQ_CONV : (conseq_conv -> conseq_conv -> conseq_conv)
Applies two consequence conversions in sequence.
THEN_CONSEQ_CONV cc1 cc2 corresponds to c1 THENC c2 for classical
conversions. Thus, if cc1 returns |- t' ==> t when applied to t,
and cc2 returns |- t'' ==> t' when applied to t', then
(THEN_CONSEQ_CONV cc1 cc2) t returns |- t'' ==> t.
THEN_CONSEQ_CONV can handle weakening as well: If cc1 returns
|- t ==> t' when applied to t, and cc2 returns |- t' ==> t''
when applied to t', then (THEN_CONSEQ_CONV cc1 cc2) t returns
|- t ==> t''. Finally, if cc1 returns |- t = t' when applied to
t, and cc2 returns |- t' = t'' when applied to t', then
(THEN_CONSEQ_CONV cc1 cc2) t returns |- t = t''. If one of the
conversions returns an equation, while the other returns an implication,
the needed implication is automatically deduced.