SELECT_EQ : (term -> thm -> thm)

- STRUCTURE
- SYNOPSIS
- Applies epsilon abstraction to both terms of an equation.
- DESCRIPTION
- Effects the extensionality of the epsilon operator @.
A |- t1 = t2 ------------------------ SELECT_EQ "x" [where x is not free in A] A |- (@x.t1) = (@x.t2)

- FAILURE
- Fails if the conclusion of the theorem is not an equation, or if the variable x is free in A.
- EXAMPLE
- Given a theorem which shows the equivalence of two distinct forms of defining the property of being an even number:A theorem giving the equivalence of the epsilon abstraction of each form is obtained:
th = |- (x MOD 2 = 0) = (?y. x = 2 * y)

- SELECT_EQ (Term `x:num`) th; > val it = |- (@x. x MOD 2 = 0) = (@x. ?y. x = 2 * y) : thm

- SEEALSO

HOL Kananaskis-14