CONSEQ_CONV_TAC : directed_conseq_conv -> tactic
STRUCTURE
ConseqConv
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
MATCH_MP_TAC
HOL
Trindemossen-1