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
```