src/FOL/IFOL.thy
changeset 2367 eba760ebe315
parent 2257 c8154379738c
child 3835 9a5a4e123859
--- 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)