diff -r bc295e3dc078 -r 928a16e02f9f src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Thu Jun 22 17:13:05 1995 +0200
@@ -41,19 +41,19 @@
 
   WO3_def "WO3 == ALL A. EX a. Ord(a) & (EX b. b <= a & A eqpoll b)"
 
-  WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   \
-\	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
+  WO4_def "WO4(m) == ALL A. EX a f. Ord(a) & domain(f)=a &   
+	             (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"
 
   WO5_def "WO5 == EX m:nat. 1 le m & WO4(m)"
 
-  WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   \
-\	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
+  WO6_def "WO6 == ALL A. EX m:nat. 1 le m & (EX a f. Ord(a) & domain(f)=a   
+	            & (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m))"
 
-  WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   \
-\	            well_ord(A,converse(R)))"
+  WO7_def "WO7 == ALL A. Finite(A) <-> (ALL R. well_ord(A,R) -->   
+	            well_ord(A,converse(R)))"
 
-  WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->  \
-\	            (EX R. well_ord(A,R))"
+  WO8_def "WO8 == ALL A. (EX f. f : (PROD X:A. X)) -->  
+	            (EX R. well_ord(A,R))"
 
 (* Axioms of Choice *)  
 
@@ -61,65 +61,65 @@
 
   AC1_def "AC1 == ALL A. 0~:A --> (EX f. f:(PROD X:A. X))"
 
-  AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   \
-\	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
+  AC2_def "AC2 == ALL A. 0~:A & pairwise_disjoint(A)   
+	            --> (EX C. ALL B:A. EX y. B Int C = {y})"
 
   AC3_def "AC3 == ALL A B. ALL f:A->B. EX g. g:(PROD x:{a:A. f`a~=0}. f`x)"
 
   AC4_def "AC4 == ALL R A B. (R<=A*B --> (EX f. f:(PROD x:domain(R). R``{x})))"
 
-  AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.   \
-\	            ALL x:domain(g). f`(g`x) = x"
+  AC5_def "AC5 == ALL A B. ALL f:A->B. EX g:range(f)->A.   
+	            ALL x:domain(g). f`(g`x) = x"
 
   AC6_def "AC6 == ALL A. 0~:A --> (PROD B:A. B)~=0"
 
-  AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   \
-\	            --> (PROD B:A. B)~=0"
+  AC7_def "AC7 == ALL A. 0~:A & (ALL B1:A. ALL B2:A. B1 eqpoll B2)   
+	            --> (PROD B:A. B)~=0"
 
-  AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)   \
-\	            --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
+  AC8_def "AC8 == ALL A. (ALL B:A. EX B1 B2. B=<B1,B2> & B1 eqpoll B2)   
+	            --> (EX f. ALL B:A. f`B : bij(fst(B),snd(B)))"
 
-  AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   \
-\	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
+  AC9_def "AC9 == ALL A. (ALL B1:A. ALL B2:A. B1 eqpoll B2) -->   
+	            (EX f. ALL B1:A. ALL B2:A. f`<B1,B2> : bij(B1,B2))"
 
-  AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   \
-\	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   \
-\	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
+  AC10_def "AC10(n) ==  ALL A. (ALL B:A. ~Finite(B)) -->   
+	            (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
+	            sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B))"
 
   AC11_def "AC11 == EX n:nat. 1 le n & AC10(n)"
 
-  AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   \
-\	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   \
-\	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
+  AC12_def "AC12 == ALL A. (ALL B:A. ~Finite(B)) -->   
+	    (EX n:nat. 1 le n & (EX f. ALL B:A. (pairwise_disjoint(f`B) &   
+	    sets_of_size_between(f`B, 2, succ(n)) & Union(f`B)=B)))"
 
-  AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   \
-\	                                  f`B <= B & f`B lepoll m)"
+  AC13_def "AC13(m) == ALL A. 0~:A --> (EX f. ALL B:A. f`B~=0 &   
+	                                  f`B <= B & f`B lepoll m)"
 
   AC14_def "AC14 == EX m:nat. 1 le m & AC13(m)"
 
-  AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   \
-\	                              f`B~=0 & f`B <= B & f`B lepoll m))"
+  AC15_def "AC15 == ALL A. 0~:A --> (EX m:nat. 1 le m & (EX f. ALL B:A.   
+	                              f`B~=0 & f`B <= B & f`B lepoll m))"
 
-  AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   \
-\	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   \
-\	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
+  AC16_def "AC16(n, k)  == ALL A. ~Finite(A) -->   
+	    (EX T. T <= {X:Pow(A). X eqpoll succ(n)} &   
+	    (ALL X:{X:Pow(A). X eqpoll succ(k)}. EX! Y. Y:T & X <= Y))"
 
-  AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   \
-\	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
+  AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}.   
+	            EX f: Pow(A)-{0} -> A. f`(g`f) : g`f"
 
-  AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->   \
-\                 ((INT a:A. UN b:B(a). X(a,b)) =   \
-\                 (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
+  AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) -->   
+                 ((INT a:A. UN b:B(a). X(a,b)) =   
+                 (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))"
 
-  AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   \
-\	            (UN f:(PROD B:A. B). INT a:A. f`a))"
+  AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) =   
+	            (UN f:(PROD B:A. B). INT a:A. f`a))"
 
 (* Auxiliary definitions used in the above definitions *)
 
-  pairwise_disjoint_def    "pairwise_disjoint(A)   \
-\			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
+  pairwise_disjoint_def    "pairwise_disjoint(A)   
+			    == ALL A1:A. ALL A2:A. A1 Int A2 ~= 0 --> A1=A2"
 
-  sets_of_size_between_def "sets_of_size_between(A,m,n)   \
-\			    == ALL B:A. m lepoll B & B lepoll n"
+  sets_of_size_between_def "sets_of_size_between(A,m,n)   
+			    == ALL B:A. m lepoll B & B lepoll n"
   
 end