src/HOL/Hilbert_Choice.thy
changeset 14872 3f2144aebd76
parent 14760 a08e916f4946
child 15131 c69542757a4d
--- a/src/HOL/Hilbert_Choice.thy	Sat Jun 05 13:06:49 2004 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Sat Jun 05 13:07:04 2004 +0200
@@ -15,8 +15,8 @@
 consts
   Eps           :: "('a => bool) => 'a"
 
-syntax (input)
-  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<epsilon>_./ _)" [0, 10] 10)
+syntax (epsilon)
+  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
 syntax (HOL)
   "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
 syntax