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