CONSEQ_CONV_TAC : directed_conseq_conv -> tactic
STRUCTURE
SYNOPSIS
Reduces the goal using a consequence conversion.
DESCRIPTION
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.
SEEALSO
HOL  Trindemossen-1