PSELECT_RULE : (thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Introduces a paired epsilon term in place of a paired existential quantifier.
- DESCRIPTION
- The inference rule PSELECT_RULE expects a theorem asserting the existence of a pair p such that t holds. The equivalent assertion that the epsilon term @p.t denotes a pair p for which t holds is returned as a theorem.
A |- ?p. t ------------------ PSELECT_RULE A |- t[(@p.t)/p]

- FAILURE
- Fails if applied to a theorem the conclusion of which is not a paired existential quantifier.
- SEEALSO

HOL Kananaskis-14