QUANT_CONSEQ_CONV : (conseq_conv -> conseq_conv)
STRUCTURE
ConseqConv
SYNOPSIS
Applies a consequence conversion to the body of an existentially or universally quantified term.
SEEALSO
QUANT_CONV
,
FORALL_CONSEQ_CONV
,
EXISTS_CONSEQ_CONV
HOL
Kananaskis-14