diff -r 768d3504d7cd -r 12dd5d2e266b Trancl.thy --- 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. :r --> :r --> :r)" comp_def (*composition of relations*) "r O s == {xz. ? x y z. xz = & :s & :r}"