----------------------------------------------------------------------
ASM_QUANT_INSTANTIATE_TAC                         (quantHeuristicsLib)
----------------------------------------------------------------------
ASM_QUANT_INSTANTIATE_TAC : quant_param list -> tactic

SYNOPSIS
A tactic to intantiate quantifiers in a term using a given list of
quantifier heuristic parameters.

DESCRIBE
This tactic is based on {quantHeuristicsLib.QUANT_INSTANTIATE_CONV}.
It tries to instantiate quantifiers. Free variables of the goal are
seen as universally quantified by this tactic. Therefore, it tries to
instantiate these free variables.
In contrast to {quantHeuristicsLib.QUANT_INSTANTIATE_TAC} this tactic
takes the assumptions of the goal into account.

SEEALSO
quantHeuristicsLib.QUANT_INSTANTIATE_CONV,
quantHeuristicsLib.QUANT_INSTANTIATE_TAC.

----------------------------------------------------------------------