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