GEN_EXISTS_TAC : string -> Parse.term Lib.frag list -> tactic
STRUCTURE
bossLib
SYNOPSIS
Instantiate a quantifier at subposition.
DESCRIPTION
GEN_EXISTS_TAC v_name i
tries to instantiate a quantifier for a variable with name
v_name
with
i
. It is short for
quantHeuristicsLib.QUANT_TAC [(v, i, [])]
. It can be seen as a generalisation of
Q.EXISTS_TAC
.
SEEALSO
EXISTS_TAC
,
QUANT_TAC
HOL
Trindemossen-1