# HG changeset patch
# User wenzelm
# Date 850219424 -3600
# Node ID eba760ebe315417081fb0da7dc110a50db24a9f2
# Parent  a163d2be1bb5b933230211fc1c88cf9ad4a701a4
fixed pris of binder syntax;

diff -r a163d2be1bb5 -r eba760ebe315 src/FOL/IFOL.thy
--- 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)