improved symbolic syntax of Eps: \<some> for mode "epsilon";
authorwenzelm
Sat Jun 05 13:07:04 2004 +0200 (2004-06-05)
changeset 148723f2144aebd76
parent 14871 1dad51c852ad
child 14873 7efc14398e82
improved symbolic syntax of Eps: \<some> for mode "epsilon";
src/HOL/Hilbert_Choice.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Jun 05 13:06:49 2004 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Jun 05 13:07:04 2004 +0200
     1.3 @@ -15,8 +15,8 @@
     1.4  consts
     1.5    Eps           :: "('a => bool) => 'a"
     1.6  
     1.7 -syntax (input)
     1.8 -  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<epsilon>_./ _)" [0, 10] 10)
     1.9 +syntax (epsilon)
    1.10 +  "_Eps"        :: "[pttrn, bool] => 'a"    ("(3\<some>_./ _)" [0, 10] 10)
    1.11  syntax (HOL)
    1.12    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3@ _./ _)" [0, 10] 10)
    1.13  syntax