src/HOL/Hilbert_Choice.thy
changeset 17702 ea88ddeafabe
parent 17420 bdcffa8d8665
child 17893 aef5a6d11c2a
--- 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