author | wenzelm |
Sat, 05 Jun 2004 13:07:04 +0200 | |
changeset 14872 | 3f2144aebd76 |
parent 14871 | 1dad51c852ad |
child 14873 | 7efc14398e82 |
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