changeset 50360 | 628b37b9e8a2 |
parent 49339 | d1fcb4de8349 |
child 51021 | 1cf4faed8b22 |
--- 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)