avoid old-style infixes;
authorwenzelm
Tue, 06 Sep 2005 16:59:51 +0200
changeset 17276 3bb24e8b2cb2
parent 17275 44d8fbc2e52d
child 17277 ab45d65bf204
avoid old-style infixes;
src/FOL/IFOL.thy
--- 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 *)