FAST_QUANT_INSTANTIATE_CONV : quant_param list -> conv
STRUCTURE
quantHeuristicsLib
SYNOPSIS
A fast version of
quantHeuristicsLib.QUANT_INSTANTIATE_CONV
. It does not preprocess the term in order to minimise the number of variable occurrences.
SEEALSO
QUANT_INSTANTIATE_CONV
,
FAST_QUANT_INSTANTIATE_TAC
HOL
Kananaskis-14