# HG changeset patch
# User nipkow
# Date 1354701934 -3600
# Node ID 3ae4376cb739d45d0de984203233326849a9725e
# Parent  da395f0e7deaa88eebcf55296dfb4125f14482f9# Parent  628b37b9e8a243b30cd41d2586deab3a70266dc8
merged

diff -r da395f0e7dea -r 3ae4376cb739 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Dec 05 10:35:58 2012 +0100
+++ b/src/HOL/HOL.thy	Wed Dec 05 11:05:34 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)