equal
deleted
inserted
replaced
15 |
15 |
16 Trancl = Lfp + Relation + |
16 Trancl = Lfp + Relation + |
17 |
17 |
18 constdefs |
18 constdefs |
19 rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [1000] 999) |
19 rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [1000] 999) |
20 "r^* == lfp(%s. id Un (r O s))" |
20 "r^* == lfp(%s. Id Un (r O s))" |
21 |
21 |
22 trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [1000] 999) |
22 trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [1000] 999) |
23 "r^+ == r O rtrancl(r)" |
23 "r^+ == r O rtrancl(r)" |
24 |
24 |
25 syntax |
25 syntax |
26 reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [1000] 999) |
26 reflcl :: "('a*'a)set => ('a*'a)set" ("(_^=)" [1000] 999) |
27 |
27 |
28 translations |
28 translations |
29 "r^=" == "r Un id" |
29 "r^=" == "r Un Id" |
30 |
30 |
31 end |
31 end |