src/FOL/IFOL.thy

--- a/src/FOL/IFOL.thy	Fri Mar 03 12:48:06 1995 +0100
+++ b/src/FOL/IFOL.thy	Tue Mar 07 13:15:25 1995 +0100
@@ -29,7 +29,6 @@
   (* Connectives *)
 
   "="           :: "['a, 'a] => o"              (infixl 50)
-  "~="          :: "['a, 'a] => o"              ("(_ ~=/ _)" [50, 51] 50)
 
   Not           :: "o => o"                     ("~ _" [40] 40)
   "&"           :: "[o, o] => o"                (infixr 35)
@@ -44,6 +43,9 @@
   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
 
 
+syntax
+  "~="          :: "['a, 'a] => o"              (infixl 50)
+
 translations
   "x ~= y"      == "~ (x = y)"