--- a/src/ZF/Trancl.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Trancl.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/trancl.thy
+(* Title: ZF/trancl.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
Transitive closure of a relation
@@ -12,6 +12,6 @@
trancl :: i=>i ("(_^+)" [100] 100) (*transitive closure*)
defs
- rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
+ rtrancl_def "r^* == lfp(field(r)*field(r), %s. id(field(r)) Un (r O s))"
trancl_def "r^+ == r O r^*"
end