changeset 21210 | c17fd2df4e9e |
parent 19756 | 61c4117345c6 |
child 21404 | eb85850d3eb7 |
--- a/src/FOL/IFOL.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/FOL/IFOL.thy Tue Nov 07 11:47:57 2006 +0100 @@ -48,10 +48,10 @@ not_equal :: "['a, 'a] => o" (infixl "~=" 50) "x ~= y == ~ (x = y)" -const_syntax (xsymbols) +notation (xsymbols) not_equal (infixl "\<noteq>" 50) -const_syntax (HTML output) +notation (HTML output) not_equal (infixl "\<noteq>" 50) syntax (xsymbols)