src/ZF/AC/Transrec2.thy
author clasohm
Tue Feb 06 12:27:17 1996 +0100 (1996-02-06)
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
permissions -rw-r--r--
expanded tabs
     1 (*  Title:      ZF/AC/Transrec2.thy
     2     ID:         $Id$
     3     Author:     Krzysztof Grabczewski
     4 
     5 Transfinite recursion introduced to handle definitions based on the three
     6 cases of ordinals.
     7 *)
     8 
     9 Transrec2 = OrdQuant + Epsilon +
    10 
    11 consts
    12   
    13   transrec2               :: [i, i, [i,i]=>i] =>i
    14 
    15 defs
    16 
    17   transrec2_def  "transrec2(alpha, a, b) ==                     
    18                          transrec(alpha, %i r. if(i=0,          
    19                                   a, if(EX j. i=succ(j),        
    20                                   b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    21                                   UN j<i. r`j)))"
    22 
    23 end