src/ZF/AC/Cardinal_aux.thy

 (* j=|A| *)
 lemma lepoll_imp_ex_le_eqpoll:
      "[| A \<lesssim> i; Ord(i) |] ==> \<exists>j. j le i & A \<approx> j"
 by (blast intro!: lepoll_cardinal_le well_ord_Memrel 
                   well_ord_cardinal_eqpoll [THEN eqpoll_sym]
-          dest: lepoll_well_ord);
+          dest: lepoll_well_ord)
 
 (* j=|A| *)
 lemma lesspoll_imp_ex_lt_eqpoll: 
      "[| A \<prec> i; Ord(i) |] ==> \<exists>j. j<i & A \<approx> j"
 by (unfold lesspoll_def, blast dest!: lepoll_imp_ex_le_eqpoll elim!: leE)

 
 (*Finally we reach this result.  Surely there's a simpler proof, as sketched
   above?*)
 lemma Un_lepoll_Inf_Ord:
      "[| A \<lesssim> i; B \<lesssim> i; ~Finite(i); Ord(i) |] ==> A Un B \<lesssim> i"
-apply (rule_tac A1 = "i" and C1 = "i" in ex_eqpoll_disjoint [THEN exE])
+apply (rule_tac A1 = i and C1 = i in ex_eqpoll_disjoint [THEN exE])
 apply (erule conjE)
 apply (drule lepoll_trans) 
 apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll])
 apply (rule Un_lepoll_Un [THEN lepoll_trans], (assumption+))
 apply (blast intro: eqpoll_refl Un_eqpoll_Inf_Ord eqpoll_imp_lepoll) 

 done
 
 lemma UN_fun_lepoll:
      "[| \<forall>b \<in> a. f`b \<lesssim> n & f`b \<subseteq> T; well_ord(T, R);   
          ~Finite(a); Ord(a); n \<in> nat |] ==> (\<Union>b \<in> a. f`b) \<lesssim> a"
-by (blast intro: UN_fun_lepoll_lemma); 
+by (blast intro: UN_fun_lepoll_lemma) 
 
 lemma UN_lepoll:
      "[| \<forall>b \<in> a. F(b) \<lesssim> n & F(b) \<subseteq> T; well_ord(T, R);   
          ~Finite(a); Ord(a); n \<in> nat |] 
       ==> (\<Union>b \<in> a. F(b)) \<lesssim> a"

 apply (rule subsetI)
 apply (erule UN_E)
 apply (rule UN_I)
  apply (rule_tac P = "%z. x \<in> F (z) " in Least_in_Ord, (assumption+))
 apply (rule DiffI, best intro: Ord_in_Ord LeastI, clarify)
-apply (erule_tac P = "%z. x \<in> F (z) " and i = "c" in less_LeastE)
+apply (erule_tac P = "%z. x \<in> F (z) " and i = c in less_LeastE)
 apply (blast intro: Ord_Least ltI)
 done
 
 lemma lepoll_imp_eqpoll_subset: 
      "a \<lesssim> X ==> \<exists>Y. Y \<subseteq> X & a \<approx> Y"