equal
deleted
inserted
replaced
47 |
47 |
48 abbreviation |
48 abbreviation |
49 not_equal :: "['a, 'a] => o" (infixl "~=" 50) |
49 not_equal :: "['a, 'a] => o" (infixl "~=" 50) |
50 "x ~= y == ~ (x = y)" |
50 "x ~= y == ~ (x = y)" |
51 |
51 |
52 abbreviation (xsymbols) |
52 const_syntax (xsymbols) |
53 not_equal1 (infixl "\<noteq>" 50) |
53 not_equal (infixl "\<noteq>" 50) |
54 "x \<noteq> y == ~ (x = y)" |
54 |
55 |
55 const_syntax (HTML output) |
56 abbreviation (HTML output) |
56 not_equal (infixl "\<noteq>" 50) |
57 not_equal2 (infixl "\<noteq>" 50) |
|
58 "not_equal2 == not_equal" |
|
59 |
57 |
60 syntax (xsymbols) |
58 syntax (xsymbols) |
61 Not :: "o => o" ("\<not> _" [40] 40) |
59 Not :: "o => o" ("\<not> _" [40] 40) |
62 "op &" :: "[o, o] => o" (infixr "\<and>" 35) |
60 "op &" :: "[o, o] => o" (infixr "\<and>" 35) |
63 "op |" :: "[o, o] => o" (infixr "\<or>" 30) |
61 "op |" :: "[o, o] => o" (infixr "\<or>" 30) |