QI_TAC : tactic
STRUCTURE
SYNOPSIS
Try to instantiate quantifiers with some default heuristics.
DESCRIPTION
QI_TAC is short for QUANT_INSTANTIATE_TAC [std_qp].
SEEALSO
HOL  Trindemossen-1