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.
fixed pris of binder syntax;
authorwenzelm
Tue, 10 Dec 1996 13:03:44 +0100
changeset 2367 eba760ebe315
parent 2366 a163d2be1bb5
child 2368 d394336997cf
fixed pris of binder syntax;
src/FOL/IFOL.thy file | annotate | diff | comparison | revisions 
--- a/src/FOL/IFOL.thy	Tue Dec 10 13:02:02 1996 +0100
+++ b/src/FOL/IFOL.thy	Tue Dec 10 13:03:44 1996 +0100
@@ -56,9 +56,9 @@
   "op |"        :: [o, o] => o                  (infixr "\\<or>" 30)
   "op -->"      :: [o, o] => o                  (infixr "\\<midarrow>\\<rightarrow>" 25)
   "op <->"      :: [o, o] => o                  (infixr "\\<leftarrow>\\<rightarrow>" 25)
-  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" 10)
-  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" 10)
-  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" 10)
+  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" [0, 10] 10)
+  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" [0, 10] 10)
+  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
   "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
isabelle