src/FOL/IFOL.thy
changeset 17276 3bb24e8b2cb2
parent 16417 9bc16273c2d4
child 17591 33d409318266
--- a/src/FOL/IFOL.thy	Tue Sep 06 16:59:50 2005 +0200
+++ b/src/FOL/IFOL.thy	Tue Sep 06 16:59:51 2005 +0200
@@ -29,13 +29,13 @@
 
   (* Connectives *)
 
-  "="           :: "['a, 'a] => o"              (infixl 50)
+  "op ="        :: "['a, 'a] => o"              (infixl "=" 50)
 
   Not           :: "o => o"                     ("~ _" [40] 40)
-  &             :: "[o, o] => o"                (infixr 35)
-  "|"           :: "[o, o] => o"                (infixr 30)
-  -->           :: "[o, o] => o"                (infixr 25)
-  <->           :: "[o, o] => o"                (infixr 25)
+  "op &"        :: "[o, o] => o"                (infixr "&" 35)
+  "op |"        :: "[o, o] => o"                (infixr "|" 30)
+  "op -->"      :: "[o, o] => o"                (infixr "-->" 25)
+  "op <->"      :: "[o, o] => o"                (infixr "<->" 25)
 
   (* Quantifiers *)