changeset 178 | 12dd5d2e266b |
parent 120 | 19facfd773de |
--- a/Trancl.thy Thu Nov 24 20:11:40 1994 +0100 +++ b/Trancl.thy Thu Nov 24 20:31:09 1994 +0100 @@ -15,7 +15,7 @@ rtrancl :: "('a * 'a)set => ('a * 'a)set" ("(_^*)" [100] 100) trancl :: "('a * 'a)set => ('a * 'a)set" ("(_^+)" [100] 100) O :: "[('b * 'c)set, ('a * 'b)set] => ('a * 'c)set" (infixr 60) -rules +defs trans_def "trans(r) == (!x y z. <x,y>:r --> <y,z>:r --> <x,z>:r)" comp_def (*composition of relations*) "r O s == {xz. ? x y z. xz = <x,z> & <x,y>:s & <y,z>:r}"