equal
deleted
inserted
replaced
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 translations |
27 translations |
28 "r^=" == "r Un Id" |
28 "r^=" == "r Un Id" |
29 |
29 |
30 syntax (xsymbols) |
30 syntax (latex) |
31 rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>*)" [1000] 999) |
31 rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>*)" [1000] 999) |
32 trancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>+)" [1000] 999) |
32 trancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>+)" [1000] 999) |
33 "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999) |
33 "_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999) |
34 |
34 |
35 end |
35 end |