src/ZF/Trancl.thy
changeset 1401 0c439768f45c
parent 753 ec86863e87c8
child 1478 2b8c2a7547ab
--- a/src/ZF/Trancl.thy	Fri Dec 08 19:48:15 1995 +0100
+++ b/src/ZF/Trancl.thy	Sat Dec 09 13:36:11 1995 +0100
@@ -8,8 +8,8 @@
 
 Trancl = Fixedpt + Perm + "mono" + Rel + 
 consts
-    rtrancl :: "i=>i"  ("(_^*)" [100] 100)  (*refl/transitive closure*)
-    trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
+    rtrancl :: i=>i  ("(_^*)" [100] 100)  (*refl/transitive closure*)
+    trancl  :: i=>i  ("(_^+)" [100] 100)  (*transitive closure*)
 
 defs
     rtrancl_def	"r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"