# HG changeset patch
# User wenzelm
# Date 1086433624 -7200
# Node ID 3f2144aebd76d8dc0a670ae7b1b59e808239eca9
# Parent  1dad51c852adaf11a8c375cfd20ca099ee437ff8
improved symbolic syntax of Eps: \<some> for mode "epsilon";

diff -r 1dad51c852ad -r 3f2144aebd76 src/HOL/Hilbert_Choice.thy
--- 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