fixed pris of binder syntax;
authorwenzelm
Tue Dec 10 13:03:44 1996 +0100 (1996-12-10)
changeset 2367eba760ebe315
parent 2366 a163d2be1bb5
child 2368 d394336997cf
fixed pris of binder syntax;
src/FOL/IFOL.thy
     1.1 --- a/src/FOL/IFOL.thy	Tue Dec 10 13:02:02 1996 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Tue Dec 10 13:03:44 1996 +0100
     1.3 @@ -56,9 +56,9 @@
     1.4    "op |"        :: [o, o] => o                  (infixr "\\<or>" 30)
     1.5    "op -->"      :: [o, o] => o                  (infixr "\\<midarrow>\\<rightarrow>" 25)
     1.6    "op <->"      :: [o, o] => o                  (infixr "\\<leftarrow>\\<rightarrow>" 25)
     1.7 -  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" 10)
     1.8 -  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" 10)
     1.9 -  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" 10)
    1.10 +  "ALL "        :: [idts, o] => o               ("(3\\<forall>_./ _)" [0, 10] 10)
    1.11 +  "EX "         :: [idts, o] => o               ("(3\\<exists>_./ _)" [0, 10] 10)
    1.12 +  "EX! "        :: [idts, o] => o               ("(3\\<exists>!_./ _)" [0, 10] 10)
    1.13    "op ~="       :: ['a, 'a] => o                (infixl "\\<noteq>" 50)
    1.14  
    1.15