equal
deleted
inserted
replaced
43 Ex :: "('a => o) => o" (binder "EX " 10) |
43 Ex :: "('a => o) => o" (binder "EX " 10) |
44 Ex1 :: "('a => o) => o" (binder "EX! " 10) |
44 Ex1 :: "('a => o) => o" (binder "EX! " 10) |
45 |
45 |
46 |
46 |
47 abbreviation |
47 abbreviation |
48 not_equal :: "['a, 'a] => o" (infixl "~=" 50) |
48 not_equal :: "['a, 'a] => o" (infixl "~=" 50) where |
49 "x ~= y == ~ (x = y)" |
49 "x ~= y == ~ (x = y)" |
50 |
50 |
51 notation (xsymbols) |
51 notation (xsymbols) |
52 not_equal (infixl "\<noteq>" 50) |
52 not_equal (infixl "\<noteq>" 50) |
53 |
53 |