PSELECT_INTRO : (thm -> thm)
STRUCTURE
PairRules
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. 
     A |- P x
   --------------  PSELECT_INTRO
    A |- P($@ P)
The returned theorem asserts that $@ P denotes some value at which P holds.
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
SELECT_INTRO, PEXISTS, PSELECT_CONV, PSELECT_ELIM, PSELECT_RULE
HOL  Trindemossen-1