src/ZF/AC/AC16_WO4.ML

--- a/src/ZF/AC/AC16_WO4.ML	Wed Apr 23 10:08:51 1997 +0200
+++ b/src/ZF/AC/AC16_WO4.ML	Wed Apr 23 10:47:36 1997 +0200
@@ -187,7 +187,7 @@
 \       ==> EX! c. c:{v:s_u(u, t_n, succ(k), y). a <= v} & b:c";
 by (etac ballE 1);
 by (fast_tac (FOL_cs addSIs [CollectI, cons_cons_subset,
-			     eqpoll_sym RS cons_cons_eqpoll]) 2);
+                             eqpoll_sym RS cons_cons_eqpoll]) 2);
 by (etac ex1E 1);
 by (res_inst_tac [("a","w")] ex1I 1);
 by (rtac conjI 1);
@@ -532,9 +532,9 @@
 by (eres_inst_tac [("x","xa")] ballE 1);
 by (fast_tac (!claset addSEs [eqpoll_sym]) 2);
 by (etac alt_ex1E 1);
-bd spec 1;
-bd spec 1;
-be mp 1;
+by (dtac spec 1);
+by (dtac spec 1);
+by (etac mp 1);
 by (Fast_tac 1);
 val unique_superset_in_MM = result();
 
@@ -669,11 +669,11 @@
 by (asm_full_simp_tac 
     (!simpset delsimps ball_simps
               addsimps [ltD,
-			ordermap_bij RS bij_converse_bij RS
-			bij_is_fun RS apply_type]) 1);
+                        ordermap_bij RS bij_converse_bij RS
+                        bij_is_fun RS apply_type]) 1);
 by (rtac eqpoll_sum_imp_Diff_lepoll 1);
 by (REPEAT (fast_tac 
-	    (FOL_cs addSDs [ltD]
+            (FOL_cs addSDs [ltD]
         addSIs [eqpoll_sum_imp_Diff_lepoll, in_LL_eqpoll_n]
         addEs [unique_superset_in_MM RS theI RS conjunct1 RS in_MM_eqpoll_n,
           in_LL_eq_Int RS equalityD1 RS (Int_lower1 RSN (2, subset_trans)),