# HG changeset patch
# User nipkow
# Date 1354701923 -3600
# Node ID 628b37b9e8a243b30cd41d2586deab3a70266dc8
# Parent  4a955d23c79b7f9b6d302ea87e3c25a43fee2ff6
\<noteq> now has the same associativity as ~= and =

diff -r 4a955d23c79b -r 628b37b9e8a2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Dec 04 22:14:59 2012 +0100
+++ b/src/HOL/HOL.thy	Wed Dec 05 11:05:23 2012 +0100
@@ -95,6 +95,9 @@
   conj  (infixr "\<and>" 35) and
   disj  (infixr "\<or>" 30) and
   implies  (infixr "\<longrightarrow>" 25) and
+  not_equal  (infixl "\<noteq>" 50)
+
+notation (xsymbols output)
   not_equal  (infix "\<noteq>" 50)
 
 notation (HTML output)