equal
deleted
inserted
replaced
14 |
14 |
15 definition |
15 definition |
16 converse :: "('a * 'b) set => ('b * 'a) set" ("(_^-1)" [1000] 999) |
16 converse :: "('a * 'b) set => ('b * 'a) set" ("(_^-1)" [1000] 999) |
17 "r^-1 == {(y, x). (x, y) : r}" |
17 "r^-1 == {(y, x). (x, y) : r}" |
18 |
18 |
19 const_syntax (xsymbols) |
19 notation (xsymbols) |
20 converse ("(_\<inverse>)" [1000] 999) |
20 converse ("(_\<inverse>)" [1000] 999) |
21 |
21 |
22 definition |
22 definition |
23 rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" (infixr "O" 75) |
23 rel_comp :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set" (infixr "O" 75) |
24 "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}" |
24 "r O s == {(x,z). EX y. (x, y) : s & (y, z) : r}" |