Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
\<epsilon>: syntax (input);
authorwenzelm
Wed, 13 Sep 2000 22:29:17 +0200
changeset 9950 879e88b1e552
parent 9949 1741a61d4b33
child 9951 5610c4acb48d
\<epsilon>: syntax (input);
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle