THEN_CONSEQ_CONV : (conseq_conv -> conseq_conv -> conseq_conv)
STRUCTURE
SYNOPSIS
Applies two consequence conversions in sequence.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1