# HG changeset patch
# User wenzelm
# Date 1126018791 -7200
# Node ID 3bb24e8b2cb27fb1f06beedfae410e7d45497ecd
# Parent  44d8fbc2e52da052c363b13ff050604de86f8dea
avoid old-style infixes;

diff -r 44d8fbc2e52d -r 3bb24e8b2cb2 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 *)