replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll
by lesspoll_trans1, lesspoll_trans2

--- a/src/ZF/AC/AC16_WO4.ML	Tue Dec 18 14:27:57 2001 +0100
+++ b/src/ZF/AC/AC16_WO4.ML	Tue Dec 18 15:03:27 2001 +0100
@@ -76,7 +76,10 @@
 Goal "[| ~(\\<exists>x \\<in> A. f`x=y); f \\<in> inj(A, B); y \\<in> B |]  \
 \     ==> (\\<lambda>a \\<in> succ(A). if(a=A, y, f`a)) \\<in> inj(succ(A), B)";
 by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1);
-by (auto_tac (claset(), simpset() addsimps [inj_is_fun RS apply_type]));
+by (force_tac (claset(), simpset() addsimps [inj_is_fun RS apply_type]) 1);
+(*this preliminary simplification prevents looping somehow*)
+by (Asm_simp_tac 1);  
+by (force_tac (claset(), simpset() addsimps []) 1);  
 qed "succ_not_lepoll_lemma";
 
 Goalw [lepoll_def, eqpoll_def, bij_def, surj_def]
@@ -251,14 +254,14 @@
 
 Goal "[| l eqpoll a; a \\<subseteq> y |] ==> y - a eqpoll y";
 by (cut_facts_tac [WO_R, Infinite, lnat] 1);
-by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll]
+by (fast_tac (empty_cs addIs [lesspoll_trans1]
         addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans,
                 Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord
                 RS le_imp_lepoll]
         addSEs [well_ord_cardinal_eqpoll,
                 well_ord_cardinal_eqpoll RS eqpoll_sym,
                 eqpoll_sym RS eqpoll_imp_lepoll,
-                n_lesspoll_nat RS lesspoll_lepoll_lesspoll,
+                n_lesspoll_nat RS lesspoll_trans2,
                 well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll
                 RS lepoll_infinite]) 1);
 qed "Diff_Finite_eqpoll";
@@ -605,3 +608,4 @@
 by (Clarify_tac 1);
 by (DEPTH_SOLVE (ares_tac [export conclusion] 1));
 qed "AC16_WO4";
+

--- a/src/ZF/AC/AC_Equiv.thy	Tue Dec 18 14:27:57 2001 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Tue Dec 18 15:03:27 2001 +0100
@@ -13,9 +13,7 @@
 *)
 
 
-AC_Equiv = CardinalArith + Univ +
-           (*NOT "Main" because that theory includes AC!!!*)
-
+AC_Equiv = Main + (*obviously not Main_ZFC*)
 
 consts
   

--- a/src/ZF/AC/Cardinal_aux.ML	Tue Dec 18 14:27:57 2001 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML	Tue Dec 18 15:03:27 2001 +0100
@@ -171,8 +171,7 @@
 (* Diff_lesspoll_eqpoll_Card                                              *)
 (* ********************************************************************** *)
 
-Goal "[| A eqpoll a; ~Finite(a); Card(a); B lesspoll a;  \
-\               A-B lesspoll a |] ==> P";
+Goal "[| A\\<approx>a; ~Finite(a); Card(a); B lesspoll a; A-B lesspoll a |] ==> P";
 by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE,
         Card_is_Ord, conjE] 1));
 by (forw_inst_tac [("j","xa")] ([lt_Ord, lt_Ord] MRS Un_upper1_le) 1
@@ -192,11 +191,10 @@
 by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_Finite] 2);
 by (fast_tac (claset()
         addDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite]) 2);
-by (dresolve_tac [ Un_lepoll_Inf_Ord] 1
-        THEN (REPEAT (assume_tac 1)));
+by (dresolve_tac [ Un_lepoll_Inf_Ord] 1 THEN (REPEAT (assume_tac 1)));
 by (fast_tac (claset() addSEs [ltE, Ord_in_Ord]) 1);
-by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RSN
-        (3, lt_Card_imp_lesspoll RS lepoll_lesspoll_lesspoll)] 1
+by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RS
+         (lt_Card_imp_lesspoll RSN (2, lesspoll_trans1))] 1
         THEN (TRYALL assume_tac));
 by (fast_tac (claset() addSDs [lesspoll_def RS def_imp_iff RS iffD1]) 1);
 qed "Diff_lesspoll_eqpoll_Card_lemma";

--- a/src/ZF/AC/DC.ML	Tue Dec 18 14:27:57 2001 +0100
+++ b/src/ZF/AC/DC.ML	Tue Dec 18 15:03:27 2001 +0100
@@ -62,8 +62,8 @@
 by (Blast_tac 2);
 by (Clarify_tac 1);
 by (forward_tac [fun_is_rel RS image_subset RS PowI RS (all_ex RS bspec)] 1);
-by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)]
-        MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1
+by (eresolve_tac [[nat_into_Ord RSN (2, image_Ord_lepoll), n_lesspoll_nat]
+        MRS lesspoll_trans1 RSN (2, impE)] 1
         THEN REPEAT (assume_tac 1));
 by (etac bexE 1);
 by (res_inst_tac [("x","cons(<n,x>, g)")] exI 1);
@@ -517,8 +517,8 @@
         addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1);
 by (etac lemmaX 1 THEN assume_tac 1);
 by (blast_tac (claset() addIs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1);
-by (fast_tac (claset() addSEs [[in_Card_imp_lesspoll, RepFun_lepoll]
-			       MRS lepoll_lesspoll_lesspoll]) 1);
+by (blast_tac (claset() addIs [lesspoll_trans1, in_Card_imp_lesspoll, 
+                               RepFun_lepoll]) 1); 
 qed "lemma";
 
 Goalw [DC_def, WO1_def] "WO1 ==> \\<forall>K. Card(K) --> DC(K)";

--- a/src/ZF/AC/WO2_AC16.ML	Tue Dec 18 14:27:57 2001 +0100
+++ b/src/ZF/AC/WO2_AC16.ML	Tue Dec 18 15:03:27 2001 +0100
@@ -145,12 +145,8 @@
 by (forward_tac [bij_is_surj RS surj_image_eq] 1);
 by (dresolve_tac [[bij_is_fun, subset_refl] MRS image_fun] 1);
 by (dresolve_tac [sym RS trans] 1 THEN (assume_tac 1));
-by (hyp_subst_tac 1);
-by (rtac lepoll_lesspoll_lesspoll 1);
-by (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1
-        THEN REPEAT (assume_tac 1));
-by (rtac UN_lepoll 1
-        THEN (TRYALL (fast_tac (claset() addSEs [lt_Ord]))));
+by (blast_tac (claset() addIs [lesspoll_trans1, UN_lepoll, lt_Ord, 
+                               lt_trans1 RSN (2, lt_Card_imp_lesspoll)]) 1); 
 qed "Union_lesspoll";
 
 (* ********************************************************************** *)

--- a/src/ZF/Cardinal.ML	Tue Dec 18 14:27:57 2001 +0100
+++ b/src/ZF/Cardinal.ML	Tue Dec 18 15:03:27 2001 +0100
@@ -169,15 +169,15 @@
 by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
 qed "lesspoll_trans";
 
+Goalw [lesspoll_def] 
+      "[| X lepoll Y; Y lesspoll Z |] ==> X lesspoll Z";
+by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
+qed "lesspoll_trans1";
+
 Goalw [lesspoll_def]
       "[| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z";
 by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
-qed "lesspoll_lepoll_lesspoll";
-
-Goalw [lesspoll_def] 
-      "[| X lesspoll Y; Z lepoll X |] ==> Z lesspoll Y";
-by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1);
-qed "lepoll_lesspoll_lesspoll";
+qed "lesspoll_trans2";
 
 
 (** LEAST -- the least number operator [from HOL/Univ.ML] **)