CONSEQ_CONV_TAC
ConseqConv.CONSEQ_CONV_TAC : directed_conseq_conv -> tactic
Reduces the goal using a consequence conversion.
CONSEQ_CONV_TAC c tries to strengthen a goal P using c to a new
goal P'. It then remains to show that P' holds.