--- a/src/ZF/Epsilon.thy Mon Feb 05 21:33:14 1996 +0100
+++ b/src/ZF/Epsilon.thy Tue Feb 06 12:27:17 1996 +0100
@@ -1,6 +1,6 @@
-(* Title: ZF/epsilon.thy
+(* Title: ZF/epsilon.thy
ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Epsilon induction and recursion
@@ -12,7 +12,7 @@
transrec :: [i, [i,i]=>i] =>i
defs
- eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
- transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
- rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
+ eclose_def "eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"
+ transrec_def "transrec(a,H) == wfrec(Memrel(eclose({a})), a, H)"
+ rank_def "rank(a) == transrec(a, %x f. UN y:x. succ(f`y))"
end