PEXISTS_TAC : (term -> tactic)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Reduces paired existentially quantified goal to one involving a specific witness.
- DESCRIPTION
- When applied to a term q and a goal ?p. t, the tactic PEXISTS_TAC reduces the goal to t[q/p].
A ?- ?p. t ============= EXISTS_TAC "q" A ?- t[q/p]

- FAILURE
- Fails unless the goal’s conclusion is a paired existential quantification and the term supplied has the same type as the quantified pair in the goal.
- EXAMPLE
- The goal:can be solved by:
?- ?(x,y). (x,y)=(1,2)

PEXISTS_TAC "(1,2)" THEN REFL_TAC

- SEEALSO

HOL Kananaskis-14