SELECT_INTRO : (thm -> thm)
STRUCTURE
Drule
SYNOPSIS
Introduces an epsilon term.
DESCRIPTION
SELECT_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
   --------------  SELECT_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.
EXAMPLE
Given the theorem 
   th1 = |- (\n. m = n)m
applying SELECT_INTRO replaces the second occurrence of m with the epsilon abstraction of the operator: 
   - val th2 = SELECT_INTRO th1;
   val th2 = |- (\n. m = n)(@n. m = n) : thm
This theorem could now be used to derive a further result: 
   - EQ_MP (BETA_CONV(concl th2)) th2;
   val it = |- m = (@n. m = n) : thm
SEEALSO
EXISTS, SELECT_CONV, SELECT_ELIM, SELECT_RULE
HOL  Trindemossen-1