src/ZF/AC/DC.thy

-(*  Title: 	ZF/AC/DC.thy
+(*  Title:      ZF/AC/DC.thy
     ID:         $Id$
-    Author: 	Krzysztof Grabczewski
+    Author:     Krzysztof Grabczewski
 
 Theory file for the proofs concernind the Axiom of Dependent Choice
 *)
 
 DC  =  AC_Equiv + Hartog + first + Cardinal_aux + "DC_lemmas" + 

   ff  :: [i, i, i, i] => i
 
 rules
 
   DC_def  "DC(a) == ALL X R. R<=Pow(X)*X &
-	   (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R)) 
-	   --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
+           (ALL Y:Pow(X). Y lesspoll a --> (EX x:X. <Y,x> : R)) 
+           --> (EX f:a->X. ALL b<a. <f``b,f`b> : R)"
 
   DC0_def "DC0 == ALL A B R. R <= A*B & R~=0 & range(R) <= domain(R) 
-	   --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
+           --> (EX f:nat->domain(R). ALL n:nat. <f`n,f`succ(n)>:R)"
 
   ff_def  "ff(b, X, Q, R) == transrec(b, %c r. 
-	                     THE x. first(x, {x:X. <r``c, x> : R}, Q))"
+                             THE x. first(x, {x:X. <r``c, x> : R}, Q))"
   
 end