src/ZF/AC/Transrec2.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
     1.1 --- a/src/ZF/AC/Transrec2.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/AC/Transrec2.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/AC/Transrec2.thy
     1.5 +(*  Title:      ZF/AC/Transrec2.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Krzysztof Grabczewski
     1.8 +    Author:     Krzysztof Grabczewski
     1.9  
    1.10  Transfinite recursion introduced to handle definitions based on the three
    1.11  cases of ordinals.
    1.12 @@ -14,10 +14,10 @@
    1.13  
    1.14  defs
    1.15  
    1.16 -  transrec2_def  "transrec2(alpha, a, b) ==   			
    1.17 -		         transrec(alpha, %i r. if(i=0,   	
    1.18 -		                  a, if(EX j. i=succ(j),   	
    1.19 -		                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    1.20 -		                  UN j<i. r`j)))"
    1.21 +  transrec2_def  "transrec2(alpha, a, b) ==                     
    1.22 +                         transrec(alpha, %i r. if(i=0,          
    1.23 +                                  a, if(EX j. i=succ(j),        
    1.24 +                                  b(THE j. i=succ(j), r`(THE j. i=succ(j))),   
    1.25 +                                  UN j<i. r`j)))"
    1.26  
    1.27  end