# HG changeset patch # User wenzelm # Date 1086433624 -7200 # Node ID 3f2144aebd76d8dc0a670ae7b1b59e808239eca9 # Parent 1dad51c852adaf11a8c375cfd20ca099ee437ff8 improved symbolic syntax of Eps: \ 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\_./ _)" [0, 10] 10) +syntax (epsilon) + "_Eps" :: "[pttrn, bool] => 'a" ("(3\_./ _)" [0, 10] 10) syntax (HOL) "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) syntax