PSELECT_INTRO : (thm -> thm)

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Introduces an epsilon term.
- DESCRIPTION
- PSELECT_INTRO takes a theorem with an applicative conclusion, say P x, and returns a theorem with the epsilon term $@ P in place of the original operand x.The returned theorem asserts that $@ P denotes some value at which P holds.
A |- P x -------------- PSELECT_INTRO A |- P($@ P)

- FAILURE
- Fails if the conclusion of the theorem is not an application.
- COMMENTS
- This function is exactly the same as SELECT_INTRO, it is duplicated in the pair library for completeness.
- SEEALSO

HOL Kananaskis-14