# HG changeset patch
# User wenzelm
# Date 968876957 -7200
# Node ID 879e88b1e5522970e8c83a7ccdb7c820fb4952a7
# Parent  1741a61d4b3373425ebea56667b596ce5b894b93
\<epsilon>: syntax (input);

diff -r 1741a61d4b33 -r 879e88b1e552 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 13 22:28:50 2000 +0200
+++ b/src/HOL/HOL.thy	Wed Sep 13 22:29:17 2000 +0200
@@ -115,13 +115,15 @@
   "op |"        :: "[bool, bool] => bool"                (infixr "\\<or>" 30)
   "op -->"      :: "[bool, bool] => bool"                (infixr "\\<midarrow>\\<rightarrow>" 25)
   "op ~="       :: "['a, 'a] => bool"                    (infixl "\\<noteq>" 50)
-  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
   "ALL "        :: "[idts, bool] => bool"                ("(3\\<forall>_./ _)" [0, 10] 10)
   "EX "         :: "[idts, bool] => bool"                ("(3\\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3\\<exists>!_./ _)" [0, 10] 10)
   "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \\<Rightarrow>/ _)" 10)
 (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
 
+syntax (input)
+  "_Eps"        :: "[pttrn, bool] => 'a"                 ("(3\\<epsilon>_./ _)" [0, 10] 10)
+
 syntax (symbols output)
   "op ~="       :: "['a, 'a] => bool"                    ("(_ \\<noteq>/ _)" [51, 51] 50)