src/ZF/AC/DC.thy
changeset 1478 2b8c2a7547ab
parent 1401 0c439768f45c
child 2469 b50b8c0eec01
     1.1 --- a/src/ZF/AC/DC.thy	Mon Feb 05 21:33:14 1996 +0100
     1.2 +++ b/src/ZF/AC/DC.thy	Tue Feb 06 12:27:17 1996 +0100
     1.3 @@ -1,6 +1,6 @@
     1.4 -(*  Title: 	ZF/AC/DC.thy
     1.5 +(*  Title:      ZF/AC/DC.thy
     1.6      ID:         $Id$
     1.7 -    Author: 	Krzysztof Grabczewski
     1.8 +    Author:     Krzysztof Grabczewski
     1.9  
    1.10  Theory file for the proofs concernind the Axiom of Dependent Choice
    1.11  *)
    1.12 @@ -16,13 +16,13 @@
    1.13  rules
    1.14  
    1.15    DC_def  "DC(a) == ALL X R. R<=Pow(X)*X &
    1.16 -	   (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R)) 
    1.17 -	   --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
    1.18 +           (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R)) 
    1.19 +           --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
    1.20  
    1.21    DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R) 
    1.22 -	   --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
    1.23 +           --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
    1.24  
    1.25    ff_def  "ff(b, X, Q, R) == transrec(b, %c r. 
    1.26 -	                     THE x. first(x, {x:X. <r``c, x> : R}, Q))"
    1.27 +                             THE x. first(x, {x:X. <r``c, x> : R}, Q))"
    1.28    
    1.29  end