GEN_EXISTS_TAC : string -> Parse.term Lib.frag list -> tactic
STRUCTURE
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
HOL  Kananaskis-13