src/FOL/IFOL.thy
changeset 19380 b808efaa5828
parent 19363 667b5ea637dd
child 19656 09be06943252
--- a/src/FOL/IFOL.thy	Sun Apr 09 18:51:11 2006 +0200
+++ b/src/FOL/IFOL.thy	Sun Apr 09 18:51:13 2006 +0200
@@ -50,12 +50,12 @@
   "x ~= y == ~ (x = y)"
 
 abbreviation (xsymbols)
-  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
+  not_equal1  (infixl "\<noteq>" 50)
   "x \<noteq> y == ~ (x = y)"
 
 abbreviation (HTML output)
-  not_equal     :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
-  "not_equal == xsymbols.not_equal"
+  not_equal2  (infixl "\<noteq>" 50)
+  "not_equal2 == not_equal"
 
 syntax (xsymbols)
   Not           :: "o => o"                     ("\<not> _" [40] 40)