QI_TAC : tactic
STRUCTURE
bossLib
SYNOPSIS
Try to instantiate quantifiers with some default heuristics.
DESCRIPTION
QI_TAC
is short for
QUANT_INSTANTIATE_TAC [std_qp]
.
SEEALSO
ASM_QI_TAC
,
QUANT_INSTANTIATE_TAC
,
ASM_QUANT_INSTANTIATE_TAC
HOL
Kananaskis-13