src/ZF/Trancl.thy
changeset 753 ec86863e87c8
parent 435 ca5356bd315a
child 1401 0c439768f45c
--- a/src/ZF/Trancl.thy	Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Trancl.thy	Tue Nov 29 00:31:31 1994 +0100
@@ -11,7 +11,7 @@
     rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
     trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
 
-rules
+defs
     rtrancl_def	"r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
     trancl_def  "r^+ == r O r^*"
 end