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