src/ZF/Epsilon.thy
changeset 6070 032babd0120b
parent 2469 b50b8c0eec01
child 13164 dfc399c684e4
     1.1 --- a/src/ZF/Epsilon.thy	Thu Jan 07 11:08:29 1999 +0100
     1.2 +++ b/src/ZF/Epsilon.thy	Thu Jan 07 18:30:55 1999 +0100
     1.3 @@ -25,4 +25,10 @@
     1.4                             b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
     1.5                             UN j<i. r`j)))"
     1.6  
     1.7 +    recursor  :: [i, [i,i]=>i, i]=>i
     1.8 +     "recursor(a,b,k) ==  transrec(k, %n f. nat_case(a, %m. b(m, f`m), n))"
     1.9 +
    1.10 +    rec  :: [i, i, [i,i]=>i]=>i
    1.11 +     "rec(k,a,b) ==  recursor(a,b,k)"
    1.12 +
    1.13  end