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