src/ZF/Epsilon.thy
changeset 1401 0c439768f45c
parent 753 ec86863e87c8
child 1478 2b8c2a7547ab
     1.1 --- a/src/ZF/Epsilon.thy	Fri Dec 08 19:48:15 1995 +0100
     1.2 +++ b/src/ZF/Epsilon.thy	Sat Dec 09 13:36:11 1995 +0100
     1.3 @@ -8,8 +8,8 @@
     1.4  
     1.5  Epsilon = Nat + "mono" +
     1.6  consts
     1.7 -    eclose,rank ::      "i=>i"
     1.8 -    transrec    ::      "[i, [i,i]=>i] =>i"
     1.9 +    eclose,rank ::      i=>i
    1.10 +    transrec    ::      [i, [i,i]=>i] =>i
    1.11  
    1.12  defs
    1.13    eclose_def	"eclose(A) == UN n:nat. nat_rec(n, A, %m r. Union(r))"