Trancl.thy
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}"