\<noteq> now has the same associativity as ~= and =
authornipkow
Wed Dec 05 11:05:23 2012 +0100 (2012-12-05)
changeset 50360628b37b9e8a2
parent 50354 4a955d23c79b
child 50361 3ae4376cb739
\<noteq> now has the same associativity as ~= and =
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Dec 04 22:14:59 2012 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Dec 05 11:05:23 2012 +0100
     1.3 @@ -95,6 +95,9 @@
     1.4    conj  (infixr "\<and>" 35) and
     1.5    disj  (infixr "\<or>" 30) and
     1.6    implies  (infixr "\<longrightarrow>" 25) and
     1.7 +  not_equal  (infixl "\<noteq>" 50)
     1.8 +
     1.9 +notation (xsymbols output)
    1.10    not_equal  (infix "\<noteq>" 50)
    1.11  
    1.12  notation (HTML output)