src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Thu Sep 29 00:58:54 2005 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 29 00:58:55 2005 +0200
@@ -34,6 +34,8 @@
 
 axioms
   someI: "P (x::'a) ==> P (SOME x. P x)"
+finalconsts
+  Eps
 
 
 constdefs