--- a/src/FOL/IFOL.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/FOL/IFOL.thy Fri Nov 17 02:20:03 2006 +0100
@@ -45,7 +45,7 @@
abbreviation
- not_equal :: "['a, 'a] => o" (infixl "~=" 50)
+ not_equal :: "['a, 'a] => o" (infixl "~=" 50) where
"x ~= y == ~ (x = y)"
notation (xsymbols)