src/ZF/AC/Transrec2.thy

expanded tabs

(*  Title:      ZF/AC/Transrec2.thy
    ID:         $Id$
    Author:     Krzysztof Grabczewski

Transfinite recursion introduced to handle definitions based on the three
cases of ordinals.
*)

Transrec2 = OrdQuant + Epsilon +

consts
  
  transrec2               :: [i, i, [i,i]=>i] =>i

defs

  transrec2_def  "transrec2(alpha, a, b) ==                     
                         transrec(alpha, %i r. if(i=0,          
                                  a, if(EX j. i=succ(j),        
                                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
                                  UN j<i. r`j)))"

end