QI_ss : ssfrag
STRUCTURE
bossLib
SYNOPSIS
Simpset-fragment for instantiating quantifiers with some default heuristics.
DESCRIPTION
QI_ss
is short for
QUANT_INST_ss [std_qp]
.
SEEALSO
QI_TAC
,
QUANT_INST_ss
HOL
Kananaskis-14