diff --git a/src/ZF/AC/AC15_WO6.thy b/src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy
+++ b/src/ZF/AC/AC15_WO6.thy
@@ -1,289 +1,289 @@
 (*  Title:      ZF/AC/AC15_WO6.thy
     Author:     Krzysztof Grabczewski
 
 The proofs needed to state that AC10, ..., AC15 are equivalent to the rest.
 We need the following:
 
 WO1 \<Longrightarrow> AC10(n) \<Longrightarrow> AC11 \<Longrightarrow> AC12 \<Longrightarrow> AC15 \<Longrightarrow> WO6
 
 In order to add the formulations AC13 and AC14 we need:
 
 AC10(succ(n)) \<Longrightarrow> AC13(n) \<Longrightarrow> AC14 \<Longrightarrow> AC15
 
 or
 
 AC1 \<Longrightarrow> AC13(1);  AC13(m) \<Longrightarrow> AC13(n) \<Longrightarrow> AC14 \<Longrightarrow> AC15    (m\<le>n)
 
 So we don't have to prove all implications of both cases.
 Moreover we don't need to prove AC13(1) \<Longrightarrow> AC1 and AC11 \<Longrightarrow> AC14 as
-Rubin \<and> Rubin do.
+Rubin & Rubin do.
 *)
 
 theory AC15_WO6
 imports HH Cardinal_aux
 begin
 
 
 (* ********************************************************************** *)
 (* Lemmas used in the proofs in which the conclusion is AC13, AC14        *)
 (* or AC15                                                                *)
 (*  - cons_times_nat_not_Finite                                           *)
 (*  - ex_fun_AC13_AC15                                                    *)
 (* ********************************************************************** *)
 
 lemma lepoll_Sigma: "A\<noteq>0 \<Longrightarrow> B \<lesssim> A*B"
   unfolding lepoll_def
 apply (erule not_emptyE)
 apply (rule_tac x = "\<lambda>z \<in> B. \<langle>x,z\<rangle>" in exI)
 apply (fast intro!: snd_conv lam_injective)
 done
 
 lemma cons_times_nat_not_Finite:
      "0\<notin>A \<Longrightarrow> \<forall>B \<in> {cons(0,x*nat). x \<in> A}. \<not>Finite(B)"
 apply clarify 
 apply (rule nat_not_Finite [THEN notE] )
 apply (subgoal_tac "x \<noteq> 0")
  apply (blast intro: lepoll_Sigma [THEN lepoll_Finite])+
 done
 
 lemma lemma1: "\<lbrakk>\<Union>(C)=A; a \<in> A\<rbrakk> \<Longrightarrow> \<exists>B \<in> C. a \<in> B \<and> B \<subseteq> A"
 by fast
 
 lemma lemma2: 
         "\<lbrakk>pairwise_disjoint(A); B \<in> A; C \<in> A; a \<in> B; a \<in> C\<rbrakk> \<Longrightarrow> B=C"
 by (unfold pairwise_disjoint_def, blast) 
 
 lemma lemma3: 
      "\<forall>B \<in> {cons(0, x*nat). x \<in> A}. pairwise_disjoint(f`B) \<and>   
              sets_of_size_between(f`B, 2, n) \<and> \<Union>(f`B)=B   
      \<Longrightarrow> \<forall>B \<in> A. \<exists>! u. u \<in> f`cons(0, B*nat) \<and> u \<subseteq> cons(0, B*nat) \<and>   
              0 \<in> u \<and> 2 \<lesssim> u \<and> u \<lesssim> n"
   unfolding sets_of_size_between_def
 apply (rule ballI)
 apply (erule_tac x="cons(0, B*nat)" in ballE)
  apply (blast dest: lemma1 intro!: lemma2, blast)
 done
 
 lemma lemma4: "\<lbrakk>A \<lesssim> i; Ord(i)\<rbrakk> \<Longrightarrow> {P(a). a \<in> A} \<lesssim> i"
   unfolding lepoll_def
 apply (erule exE)
 apply (rule_tac x = "\<lambda>x \<in> RepFun(A,P). \<mu> j. \<exists>a\<in>A. x=P(a) \<and> f`a=j" 
        in exI)
 apply (rule_tac d = "\<lambda>y. P (converse (f) `y) " in lam_injective)
 apply (erule RepFunE)
 apply (frule inj_is_fun [THEN apply_type], assumption)
 apply (fast intro: LeastI2 elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
 apply (erule RepFunE)
 apply (rule LeastI2)
   apply fast
  apply (fast elim!: Ord_in_Ord inj_is_fun [THEN apply_type])
 apply (fast elim: sym left_inverse [THEN ssubst])
 done
 
 lemma lemma5_1:
      "\<lbrakk>B \<in> A; 2 \<lesssim> u(B)\<rbrakk> \<Longrightarrow> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<noteq> 0"
 apply simp
 apply (fast dest: lepoll_Diff_sing 
             elim: lepoll_trans [THEN succ_lepoll_natE] ssubst
             intro!: lepoll_refl)
 done
 
 lemma lemma5_2:
      "\<lbrakk>B \<in> A; u(B) \<subseteq> cons(0, B*nat)\<rbrakk>   
       \<Longrightarrow> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<subseteq> B"
 apply auto 
 done
 
 lemma lemma5_3:
      "\<lbrakk>n \<in> nat; B \<in> A; 0 \<in> u(B); u(B) \<lesssim> succ(n)\<rbrakk>   
       \<Longrightarrow> (\<lambda>x \<in> A. {fst(x). x \<in> u(x)-{0}})`B \<lesssim> n"
 apply simp
 apply (fast elim!: Diff_lepoll [THEN lemma4 [OF _ nat_into_Ord]])
 done
 
 lemma ex_fun_AC13_AC15:
      "\<lbrakk>\<forall>B \<in> {cons(0, x*nat). x \<in> A}.   
                 pairwise_disjoint(f`B) \<and>   
                 sets_of_size_between(f`B, 2, succ(n)) \<and> \<Union>(f`B)=B; 
          n \<in> nat\<rbrakk>   
       \<Longrightarrow> \<exists>f. \<forall>B \<in> A. f`B \<noteq> 0 \<and> f`B \<subseteq> B \<and> f`B \<lesssim> n"
 by (fast del: subsetI notI
          dest!: lemma3 theI intro!: lemma5_1 lemma5_2 lemma5_3)
 
 
 (* ********************************************************************** *)
 (* The target proofs                                                      *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
 (* AC10(n) \<Longrightarrow> AC11                                                       *)
 (* ********************************************************************** *)
 
 theorem AC10_AC11: "\<lbrakk>n \<in> nat; 1\<le>n; AC10(n)\<rbrakk> \<Longrightarrow> AC11"
 by (unfold AC10_def AC11_def, blast)
 
 (* ********************************************************************** *)
 (* AC11 \<Longrightarrow> AC12                                                          *)
 (* ********************************************************************** *)
 
 theorem AC11_AC12: "AC11 \<Longrightarrow> AC12"
 by (unfold AC10_def AC11_def AC11_def AC12_def, blast)
 
 (* ********************************************************************** *)
 (* AC12 \<Longrightarrow> AC15                                                          *)
 (* ********************************************************************** *)
 
 theorem AC12_AC15: "AC12 \<Longrightarrow> AC15"
   unfolding AC12_def AC15_def
 apply (blast del: ballI 
              intro!: cons_times_nat_not_Finite ex_fun_AC13_AC15)
 done
 
 (* ********************************************************************** *)
 (* AC15 \<Longrightarrow> WO6                                                           *)
 (* ********************************************************************** *)
 
 lemma OUN_eq_UN: "Ord(x) \<Longrightarrow> (\<Union>a<x. F(a)) = (\<Union>a \<in> x. F(a))"
 by (fast intro!: ltI dest!: ltD)
 
 lemma AC15_WO6_aux1:
      "\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 \<and> f`x \<subseteq> x \<and> f`x \<lesssim> m 
       \<Longrightarrow> (\<Union>i<\<mu> x. HH(f,A,x)={A}. HH(f,A,i)) = A"
 apply (simp add: Ord_Least [THEN OUN_eq_UN])
 apply (rule equalityI)
 apply (fast dest!: less_Least_subset_x)
 apply (blast del: subsetI 
            intro!: f_subsets_imp_UN_HH_eq_x [THEN Diff_eq_0_iff [THEN iffD1]])
 done
 
 lemma AC15_WO6_aux2:
      "\<forall>x \<in> Pow(A)-{0}. f`x\<noteq>0 \<and> f`x \<subseteq> x \<and> f`x \<lesssim> m 
       \<Longrightarrow> \<forall>x < (\<mu> x. HH(f,A,x)={A}). HH(f,A,x) \<lesssim> m"
 apply (rule oallI)
 apply (drule ltD [THEN less_Least_subset_x])
 apply (frule HH_subset_imp_eq)
 apply (erule ssubst)
 apply (blast dest!: HH_subset_x_imp_subset_Diff_UN [THEN not_emptyI2])
         (*but can't use del: DiffE despite the obvious conflict*)
 done
 
 theorem AC15_WO6: "AC15 \<Longrightarrow> WO6"
   unfolding AC15_def WO6_def
 apply (rule allI)
 apply (erule_tac x = "Pow (A) -{0}" in allE)
 apply (erule impE, fast)
 apply (elim bexE conjE exE)
 apply (rule bexI)
  apply (rule conjI, assumption)
  apply (rule_tac x = "\<mu> i. HH (f,A,i) ={A}" in exI)
  apply (rule_tac x = "\<lambda>j \<in> (\<mu> i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
  apply (simp_all add: ltD)
 apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
             elim!: less_Least_subset_x AC15_WO6_aux1 AC15_WO6_aux2) 
 done
 
 
 (* ********************************************************************** *)
 (* The proof needed in the first case, not in the second                  *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
 (* AC10(n) \<Longrightarrow> AC13(n-1)  if 2\<le>n                                       *)
 (*                                                                        *)
 (* Because of the change to the formal definition of AC10(n) we prove     *)
 (* the following obviously equivalent theorem \<in>                           *)
 (* AC10(n) implies AC13(n) for (1\<le>n)                                   *)
 (* ********************************************************************** *)
 
 theorem AC10_AC13: "\<lbrakk>n \<in> nat; 1\<le>n; AC10(n)\<rbrakk> \<Longrightarrow> AC13(n)"
 apply (unfold AC10_def AC13_def, safe)
 apply (erule allE) 
 apply (erule impE [OF _ cons_times_nat_not_Finite], assumption) 
 apply (fast elim!: impE [OF _ cons_times_nat_not_Finite] 
             dest!: ex_fun_AC13_AC15)
 done
 
 (* ********************************************************************** *)
 (* The proofs needed in the second case, not in the first                 *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
 (* AC1 \<Longrightarrow> AC13(1)                                                        *)
 (* ********************************************************************** *)
 
 lemma AC1_AC13: "AC1 \<Longrightarrow> AC13(1)"
   unfolding AC1_def AC13_def
 apply (rule allI)
 apply (erule allE)
 apply (rule impI)
 apply (drule mp, assumption) 
 apply (elim exE)
 apply (rule_tac x = "\<lambda>x \<in> A. {f`x}" in exI)
 apply (simp add: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll])
 done
 
 (* ********************************************************************** *)
 (* AC13(m) \<Longrightarrow> AC13(n) for m \<subseteq> n                                         *)
 (* ********************************************************************** *)
 
 lemma AC13_mono: "\<lbrakk>m\<le>n; AC13(m)\<rbrakk> \<Longrightarrow> AC13(n)"
   unfolding AC13_def
 apply (drule le_imp_lepoll)
 apply (fast elim!: lepoll_trans)
 done
 
 (* ********************************************************************** *)
 (* The proofs necessary for both cases                                    *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
 (* AC13(n) \<Longrightarrow> AC14  if 1 \<subseteq> n                                            *)
 (* ********************************************************************** *)
 
 theorem AC13_AC14: "\<lbrakk>n \<in> nat; 1\<le>n; AC13(n)\<rbrakk> \<Longrightarrow> AC14"
 by (unfold AC13_def AC14_def, auto)
 
 (* ********************************************************************** *)
 (* AC14 \<Longrightarrow> AC15                                                          *)
 (* ********************************************************************** *)
 
 theorem AC14_AC15: "AC14 \<Longrightarrow> AC15"
 by (unfold AC13_def AC14_def AC15_def, fast)
 
 (* ********************************************************************** *)
-(* The redundant proofs; however cited by Rubin \<and> Rubin                   *)
+(* The redundant proofs; however cited by Rubin & Rubin                   *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
 (* AC13(1) \<Longrightarrow> AC1                                                        *)
 (* ********************************************************************** *)
 
 lemma lemma_aux: "\<lbrakk>A\<noteq>0; A \<lesssim> 1\<rbrakk> \<Longrightarrow> \<exists>a. A={a}"
 by (fast elim!: not_emptyE lepoll_1_is_sing)
 
 lemma AC13_AC1_lemma:
      "\<forall>B \<in> A. f(B)\<noteq>0 \<and> f(B)<=B \<and> f(B) \<lesssim> 1   
       \<Longrightarrow> (\<lambda>x \<in> A. THE y. f(x)={y}) \<in> (\<Prod>X \<in> A. X)"
 apply (rule lam_type)
 apply (drule bspec, assumption)
 apply (elim conjE)
 apply (erule lemma_aux [THEN exE], assumption)
 apply (simp add: the_equality)
 done
 
 theorem AC13_AC1: "AC13(1) \<Longrightarrow> AC1"
   unfolding AC13_def AC1_def
 apply (fast elim!: AC13_AC1_lemma)
 done
 
 (* ********************************************************************** *)
 (* AC11 \<Longrightarrow> AC14                                                          *)
 (* ********************************************************************** *)
 
 theorem AC11_AC14: "AC11 \<Longrightarrow> AC14"
   unfolding AC11_def AC14_def
 apply (fast intro!: AC10_AC13)
 done
 
 end
 
diff --git a/src/ZF/AC/AC17_AC1.thy b/src/ZF/AC/AC17_AC1.thy
--- a/src/ZF/AC/AC17_AC1.thy
+++ b/src/ZF/AC/AC17_AC1.thy
@@ -1,301 +1,301 @@
 (*  Title:      ZF/AC/AC17_AC1.thy
     Author:     Krzysztof Grabczewski
 
 The equivalence of AC0, AC1 and AC17
 
 Also, the proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent
 to AC0 and AC1.
 *)
 
 theory AC17_AC1
 imports HH
 begin
 
 
 (** AC0 is equivalent to AC1.  
-    AC0 comes from Suppes, AC1 from Rubin \<and> Rubin **)
+    AC0 comes from Suppes, AC1 from Rubin & Rubin **)
 
 lemma AC0_AC1_lemma: "\<lbrakk>f:(\<Prod>X \<in> A. X); D \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>g. g:(\<Prod>X \<in> D. X)"
 by (fast intro!: lam_type apply_type)
 
 lemma AC0_AC1: "AC0 \<Longrightarrow> AC1"
   unfolding AC0_def AC1_def
 apply (blast intro: AC0_AC1_lemma)
 done
 
 lemma AC1_AC0: "AC1 \<Longrightarrow> AC0"
 by (unfold AC0_def AC1_def, blast)
 
 
 (**** The proof of AC1 \<Longrightarrow> AC17 ****)
 
 lemma AC1_AC17_lemma: "f \<in> (\<Prod>X \<in> Pow(A) - {0}. X) \<Longrightarrow> f \<in> (Pow(A) - {0} -> A)"
 apply (rule Pi_type, assumption)
 apply (drule apply_type, assumption, fast)
 done
 
 lemma AC1_AC17: "AC1 \<Longrightarrow> AC17"
   unfolding AC1_def AC17_def
 apply (rule allI)
 apply (rule ballI)
 apply (erule_tac x = "Pow (A) -{0}" in allE)
 apply (erule impE, fast)
 apply (erule exE)
 apply (rule bexI)
 apply (erule_tac [2] AC1_AC17_lemma)
 apply (rule apply_type, assumption)
 apply (fast dest!: AC1_AC17_lemma elim!: apply_type)
 done
 
 
 (**** The proof of AC17 \<Longrightarrow> AC1 ****)
 
 (* *********************************************************************** *)
 (* more properties of HH                                                   *)
 (* *********************************************************************** *)
 
 lemma UN_eq_imp_well_ord:
      "\<lbrakk>x - (\<Union>j \<in> \<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, i) = {x}.  
         HH(\<lambda>X \<in> Pow(x)-{0}. {f`X}, x, j)) = 0;   
         f \<in> Pow(x)-{0} -> x\<rbrakk>   
         \<Longrightarrow> \<exists>r. well_ord(x,r)"
 apply (rule exI)
 apply (erule well_ord_rvimage 
         [OF bij_Least_HH_x [THEN bij_converse_bij, THEN bij_is_inj] 
             Ord_Least [THEN well_ord_Memrel]], assumption)
 done
 
 (* *********************************************************************** *)
 (* theorems closer to the proof                                            *)
 (* *********************************************************************** *)
 
 lemma not_AC1_imp_ex:
      "\<not>AC1 \<Longrightarrow> \<exists>A. \<forall>f \<in> Pow(A)-{0} -> A. \<exists>u \<in> Pow(A)-{0}. f`u \<notin> u"
   unfolding AC1_def
 apply (erule swap)
 apply (rule allI)
 apply (erule swap)
 apply (rule_tac x = "\<Union>(A)" in exI)
 apply (blast intro: lam_type)
 done
 
 lemma AC17_AC1_aux1:
      "\<lbrakk>\<forall>f \<in> Pow(x) - {0} -> x. \<exists>u \<in> Pow(x) - {0}. f`u\<notin>u;   
          \<exists>f \<in> Pow(x)-{0}->x.  
             x - (\<Union>a \<in> (\<mu> i. HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,i)={x}).   
             HH(\<lambda>X \<in> Pow(x)-{0}. {f`X},x,a)) = 0\<rbrakk>  
         \<Longrightarrow> P"
 apply (erule bexE)
 apply (erule UN_eq_imp_well_ord [THEN exE], assumption)
 apply (erule ex_choice_fun_Pow [THEN exE])
 apply (erule ballE) 
 apply (fast intro: apply_type del: DiffE)
 apply (erule notE)
 apply (rule Pi_type, assumption)
 apply (blast dest: apply_type) 
 done
 
 lemma AC17_AC1_aux2:
       "\<not> (\<exists>f \<in> Pow(x)-{0}->x. x - F(f) = 0)   
        \<Longrightarrow> (\<lambda>f \<in> Pow(x)-{0}->x . x - F(f))   
            \<in> (Pow(x) -{0} -> x) -> Pow(x) - {0}"
 by (fast intro!: lam_type dest!: Diff_eq_0_iff [THEN iffD1])
 
 lemma AC17_AC1_aux3:
      "\<lbrakk>f`Z \<in> Z; Z \<in> Pow(x)-{0}\<rbrakk> 
       \<Longrightarrow> (\<lambda>X \<in> Pow(x)-{0}. {f`X})`Z \<in> Pow(Z)-{0}"
 by auto
 
 lemma AC17_AC1_aux4:
      "\<exists>f \<in> F. f`((\<lambda>f \<in> F. Q(f))`f) \<in> (\<lambda>f \<in> F. Q(f))`f   
       \<Longrightarrow> \<exists>f \<in> F. f`Q(f) \<in> Q(f)"
 by simp
 
 lemma AC17_AC1: "AC17 \<Longrightarrow> AC1"
   unfolding AC17_def
 apply (rule classical)
 apply (erule not_AC1_imp_ex [THEN exE])
 apply (case_tac 
        "\<exists>f \<in> Pow(x)-{0} -> x. 
         x - (\<Union>a \<in> (\<mu> i. HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,i) ={x}) . HH (\<lambda>X \<in> Pow (x) -{0}. {f`X},x,a)) = 0")
 apply (erule AC17_AC1_aux1, assumption)
 apply (drule AC17_AC1_aux2)
 apply (erule allE)
 apply (drule bspec, assumption)
 apply (drule AC17_AC1_aux4)
 apply (erule bexE)
 apply (drule apply_type, assumption)
 apply (simp add: HH_Least_eq_x del: Diff_iff ) 
 apply (drule AC17_AC1_aux3, assumption) 
 apply (fast dest!: subst_elem [OF _ HH_Least_eq_x [symmetric]]
                    f_subset_imp_HH_subset elim!: mem_irrefl)
 done
 
 
 (* **********************************************************************
     AC1 \<Longrightarrow> AC2 \<Longrightarrow> AC1
     AC1 \<Longrightarrow> AC4 \<Longrightarrow> AC3 \<Longrightarrow> AC1
     AC4 \<Longrightarrow> AC5 \<Longrightarrow> AC4
     AC1 \<longleftrightarrow> AC6
 ************************************************************************* *)
 
 (* ********************************************************************** *)
 (* AC1 \<Longrightarrow> AC2                                                            *)
 (* ********************************************************************** *)
 
 lemma AC1_AC2_aux1:
      "\<lbrakk>f:(\<Prod>X \<in> A. X);  B \<in> A;  0\<notin>A\<rbrakk> \<Longrightarrow> {f`B} \<subseteq> B \<inter> {f`C. C \<in> A}"
 by (fast elim!: apply_type)
 
 lemma AC1_AC2_aux2: 
         "\<lbrakk>pairwise_disjoint(A); B \<in> A; C \<in> A; D \<in> B; D \<in> C\<rbrakk> \<Longrightarrow> f`B = f`C"
 by (unfold pairwise_disjoint_def, fast)
 
 lemma AC1_AC2: "AC1 \<Longrightarrow> AC2"
   unfolding AC1_def AC2_def
 apply (rule allI)
 apply (rule impI)  
 apply (elim asm_rl conjE allE exE impE, assumption)
 apply (intro exI ballI equalityI)
 prefer 2 apply (rule AC1_AC2_aux1, assumption+)
 apply (fast elim!: AC1_AC2_aux2 elim: apply_type)
 done
 
 
 (* ********************************************************************** *)
 (* AC2 \<Longrightarrow> AC1                                                            *)
 (* ********************************************************************** *)
 
 lemma AC2_AC1_aux1: "0\<notin>A \<Longrightarrow> 0 \<notin> {B*{B}. B \<in> A}"
 by (fast dest!: sym [THEN Sigma_empty_iff [THEN iffD1]])
 
 lemma AC2_AC1_aux2: "\<lbrakk>X*{X} \<inter> C = {y}; X \<in> A\<rbrakk>   
                \<Longrightarrow> (THE y. X*{X} \<inter> C = {y}): X*A"
 apply (rule subst_elem [of y])
 apply (blast elim!: equalityE)
 apply (auto simp add: singleton_eq_iff) 
 done
 
 lemma AC2_AC1_aux3:
      "\<forall>D \<in> {E*{E}. E \<in> A}. \<exists>y. D \<inter> C = {y}   
       \<Longrightarrow> (\<lambda>x \<in> A. fst(THE z. (x*{x} \<inter> C = {z}))) \<in> (\<Prod>X \<in> A. X)"
 apply (rule lam_type)
 apply (drule bspec, blast)
 apply (blast intro: AC2_AC1_aux2 fst_type)
 done
 
 lemma AC2_AC1: "AC2 \<Longrightarrow> AC1"
   unfolding AC1_def AC2_def pairwise_disjoint_def
 apply (intro allI impI)
 apply (elim allE impE)
 prefer 2 apply (fast elim!: AC2_AC1_aux3) 
 apply (blast intro!: AC2_AC1_aux1)
 done
 
 
 (* ********************************************************************** *)
 (* AC1 \<Longrightarrow> AC4                                                            *)
 (* ********************************************************************** *)
 
 lemma empty_notin_images: "0 \<notin> {R``{x}. x \<in> domain(R)}"
 by blast
 
 lemma AC1_AC4: "AC1 \<Longrightarrow> AC4"
   unfolding AC1_def AC4_def
 apply (intro allI impI)
 apply (drule spec, drule mp [OF _ empty_notin_images]) 
 apply (best intro!: lam_type elim!: apply_type)
 done
 
 
 (* ********************************************************************** *)
 (* AC4 \<Longrightarrow> AC3                                                            *)
 (* ********************************************************************** *)
 
 lemma AC4_AC3_aux1: "f \<in> A->B \<Longrightarrow> (\<Union>z \<in> A. {z}*f`z) \<subseteq> A*\<Union>(B)"
 by (fast dest!: apply_type)
 
 lemma AC4_AC3_aux2: "domain(\<Union>z \<in> A. {z}*f(z)) = {a \<in> A. f(a)\<noteq>0}"
 by blast
 
 lemma AC4_AC3_aux3: "x \<in> A \<Longrightarrow> (\<Union>z \<in> A. {z}*f(z))``{x} = f(x)"
 by fast
 
 lemma AC4_AC3: "AC4 \<Longrightarrow> AC3"
   unfolding AC3_def AC4_def
 apply (intro allI ballI)
 apply (elim allE impE)
 apply (erule AC4_AC3_aux1)
 apply (simp add: AC4_AC3_aux2 AC4_AC3_aux3 cong add: Pi_cong)
 done
 
 (* ********************************************************************** *)
 (* AC3 \<Longrightarrow> AC1                                                            *)
 (* ********************************************************************** *)
 
 lemma AC3_AC1_lemma:
      "b\<notin>A \<Longrightarrow> (\<Prod>x \<in> {a \<in> A. id(A)`a\<noteq>b}. id(A)`x) = (\<Prod>x \<in> A. x)"
 apply (simp add: id_def cong add: Pi_cong)
 apply (rule_tac b = A in subst_context, fast)
 done
 
 lemma AC3_AC1: "AC3 \<Longrightarrow> AC1"
   unfolding AC1_def AC3_def
 apply (fast intro!: id_type elim: AC3_AC1_lemma [THEN subst])
 done
 
 (* ********************************************************************** *)
 (* AC4 \<Longrightarrow> AC5                                                            *)
 (* ********************************************************************** *)
 
 lemma AC4_AC5: "AC4 \<Longrightarrow> AC5"
   unfolding range_def AC4_def AC5_def
 apply (intro allI ballI)
 apply (elim allE impE)
 apply (erule fun_is_rel [THEN converse_type])
 apply (erule exE)
 apply (rename_tac g)
 apply (rule_tac x=g in bexI)
 apply (blast dest: apply_equality range_type) 
 apply (blast intro: Pi_type dest: apply_type fun_is_rel)
 done
 
 
 (* ********************************************************************** *)
-(* AC5 \<Longrightarrow> AC4, Rubin \<and> Rubin, p. 11                                      *)
+(* AC5 \<Longrightarrow> AC4, Rubin & Rubin, p. 11                                      *)
 (* ********************************************************************** *)
 
 lemma AC5_AC4_aux1: "R \<subseteq> A*B \<Longrightarrow> (\<lambda>x \<in> R. fst(x)) \<in> R -> A"
 by (fast intro!: lam_type fst_type)
 
 lemma AC5_AC4_aux2: "R \<subseteq> A*B \<Longrightarrow> range(\<lambda>x \<in> R. fst(x)) = domain(R)"
 by (unfold lam_def, force)
 
 lemma AC5_AC4_aux3: "\<lbrakk>\<exists>f \<in> A->C. P(f,domain(f)); A=B\<rbrakk> \<Longrightarrow>  \<exists>f \<in> B->C. P(f,B)"
 apply (erule bexE)
 apply (frule domain_of_fun, fast)
 done
 
 lemma AC5_AC4_aux4: "\<lbrakk>R \<subseteq> A*B; g \<in> C->R; \<forall>x \<in> C. (\<lambda>z \<in> R. fst(z))` (g`x) = x\<rbrakk>  
                 \<Longrightarrow> (\<lambda>x \<in> C. snd(g`x)): (\<Prod>x \<in> C. R``{x})"
 apply (rule lam_type)
 apply (force dest: apply_type)
 done
 
 lemma AC5_AC4: "AC5 \<Longrightarrow> AC4"
 apply (unfold AC4_def AC5_def, clarify)
 apply (elim allE ballE)
 apply (drule AC5_AC4_aux3 [OF _ AC5_AC4_aux2], assumption)
 apply (fast elim!: AC5_AC4_aux4)
 apply (blast intro: AC5_AC4_aux1) 
 done
 
 
 (* ********************************************************************** *)
 (* AC1 \<longleftrightarrow> AC6                                                            *)
 (* ********************************************************************** *)
 
 lemma AC1_iff_AC6: "AC1 \<longleftrightarrow> AC6"
 by (unfold AC1_def AC6_def, blast)
 
 end
diff --git a/src/ZF/AC/AC7_AC9.thy b/src/ZF/AC/AC7_AC9.thy
--- a/src/ZF/AC/AC7_AC9.thy
+++ b/src/ZF/AC/AC7_AC9.thy
@@ -1,169 +1,169 @@
 (*  Title:      ZF/AC/AC7_AC9.thy
     Author:     Krzysztof Grabczewski
 
 The proofs needed to state that AC7, AC8 and AC9 are equivalent to the previous
 instances of AC.
 *)
 
 theory AC7_AC9
 imports AC_Equiv
 begin
 
 (* ********************************************************************** *)
 (* Lemmas used in the proofs AC7 \<Longrightarrow> AC6 and AC9 \<Longrightarrow> AC1                  *)
 (*  - Sigma_fun_space_not0                                                *)
 (*  - Sigma_fun_space_eqpoll                                              *)
 (* ********************************************************************** *)
 
 lemma Sigma_fun_space_not0: "\<lbrakk>0\<notin>A; B \<in> A\<rbrakk> \<Longrightarrow> (nat->\<Union>(A)) * B \<noteq> 0"
 by (blast dest!: Sigma_empty_iff [THEN iffD1] Union_empty_iff [THEN iffD1])
 
 lemma inj_lemma: 
         "C \<in> A \<Longrightarrow> (\<lambda>g \<in> (nat->\<Union>(A))*C.   
                 (\<lambda>n \<in> nat. if(n=0, snd(g), fst(g)`(n #- 1))))   
                 \<in> inj((nat->\<Union>(A))*C, (nat->\<Union>(A)) ) "
   unfolding inj_def
 apply (rule CollectI)
 apply (fast intro!: lam_type if_type apply_type fst_type snd_type, auto) 
 apply (rule fun_extension, assumption+)
 apply (drule lam_eqE [OF _ nat_succI], assumption, simp) 
 apply (drule lam_eqE [OF _ nat_0I], simp) 
 done
 
 lemma Sigma_fun_space_eqpoll:
      "\<lbrakk>C \<in> A; 0\<notin>A\<rbrakk> \<Longrightarrow> (nat->\<Union>(A)) * C \<approx> (nat->\<Union>(A))"
 apply (rule eqpollI)
 apply (simp add: lepoll_def)
 apply (fast intro!: inj_lemma)
 apply (fast elim!: prod_lepoll_self not_sym [THEN not_emptyE] subst_elem 
             elim: swap)
 done
 
 
 (* ********************************************************************** *)
 (* AC6 \<Longrightarrow> AC7                                                            *)
 (* ********************************************************************** *)
 
 lemma AC6_AC7: "AC6 \<Longrightarrow> AC7"
 by (unfold AC6_def AC7_def, blast)
 
 (* ********************************************************************** *)
-(* AC7 \<Longrightarrow> AC6, Rubin \<and> Rubin p. 12, Theorem 2.8                          *)
+(* AC7 \<Longrightarrow> AC6, Rubin & Rubin p. 12, Theorem 2.8                          *)
 (* The case of the empty family of sets added in order to complete        *)
 (* the proof.                                                             *)
 (* ********************************************************************** *)
 
 lemma lemma1_1: "y \<in> (\<Prod>B \<in> A. Y*B) \<Longrightarrow> (\<lambda>B \<in> A. snd(y`B)) \<in> (\<Prod>B \<in> A. B)"
 by (fast intro!: lam_type snd_type apply_type)
 
 lemma lemma1_2:
      "y \<in> (\<Prod>B \<in> {Y*C. C \<in> A}. B) \<Longrightarrow> (\<lambda>B \<in> A. y`(Y*B)) \<in> (\<Prod>B \<in> A. Y*B)"
 apply (fast intro!: lam_type apply_type)
 done
 
 lemma AC7_AC6_lemma1:
      "(\<Prod>B \<in> {(nat->\<Union>(A))*C. C \<in> A}. B) \<noteq> 0 \<Longrightarrow> (\<Prod>B \<in> A. B) \<noteq> 0"
 by (fast intro!: equals0I lemma1_1 lemma1_2)
 
 lemma AC7_AC6_lemma2: "0 \<notin> A \<Longrightarrow> 0 \<notin> {(nat -> \<Union>(A)) * C. C \<in> A}"
 by (blast dest: Sigma_fun_space_not0)
 
 lemma AC7_AC6: "AC7 \<Longrightarrow> AC6"
   unfolding AC6_def AC7_def
 apply (rule allI)
 apply (rule impI)
 apply (case_tac "A=0", simp)
 apply (rule AC7_AC6_lemma1)
 apply (erule allE) 
 apply (blast del: notI
              intro!: AC7_AC6_lemma2 intro: eqpoll_sym eqpoll_trans 
                     Sigma_fun_space_eqpoll)
 done
 
 
 (* ********************************************************************** *)
 (* AC1 \<Longrightarrow> AC8                                                            *)
 (* ********************************************************************** *)
 
 lemma AC1_AC8_lemma1: 
         "\<forall>B \<in> A. \<exists>B1 B2. B=\<langle>B1,B2\<rangle> \<and> B1 \<approx> B2   
         \<Longrightarrow> 0 \<notin> { bij(fst(B),snd(B)). B \<in> A }"
 apply (unfold eqpoll_def, auto)
 done
 
 lemma AC1_AC8_lemma2:
      "\<lbrakk>f \<in> (\<Prod>X \<in> RepFun(A,p). X); D \<in> A\<rbrakk> \<Longrightarrow> (\<lambda>x \<in> A. f`p(x))`D \<in> p(D)" 
 apply (simp, fast elim!: apply_type)
 done
 
 lemma AC1_AC8: "AC1 \<Longrightarrow> AC8"
   unfolding AC1_def AC8_def
 apply (fast dest: AC1_AC8_lemma1 AC1_AC8_lemma2)
 done
 
 
 (* ********************************************************************** *)
 (* AC8 \<Longrightarrow> AC9                                                            *)
-(*  - this proof replaces the following two from Rubin \<and> Rubin:           *)
+(*  - this proof replaces the following two from Rubin & Rubin:           *)
 (*    AC8 \<Longrightarrow> AC1 and AC1 \<Longrightarrow> AC9                                         *)
 (* ********************************************************************** *)
 
 lemma AC8_AC9_lemma:
      "\<forall>B1 \<in> A. \<forall>B2 \<in> A. B1 \<approx> B2 
       \<Longrightarrow> \<forall>B \<in> A*A. \<exists>B1 B2. B=\<langle>B1,B2\<rangle> \<and> B1 \<approx> B2"
 by fast
 
 lemma AC8_AC9: "AC8 \<Longrightarrow> AC9"
   unfolding AC8_def AC9_def
 apply (intro allI impI)
 apply (erule allE)
 apply (erule impE, erule AC8_AC9_lemma, force) 
 done
 
 
 (* ********************************************************************** *)
 (* AC9 \<Longrightarrow> AC1                                                            *)
 (* The idea of this proof comes from "Equivalents of the Axiom of Choice" *)
-(* by Rubin \<and> Rubin. But (x * y) is not necessarily equipollent to        *)
+(* by Rubin & Rubin. But (x * y) is not necessarily equipollent to        *)
 (* (x * y) \<union> {0} when y is a set of total functions acting from nat to   *)
 (* \<Union>(A) -- therefore we have used the set (y * nat) instead of y.     *)
 (* ********************************************************************** *)
 
 lemma snd_lepoll_SigmaI: "b \<in> B \<Longrightarrow> X \<lesssim> B \<times> X"
 by (blast intro: lepoll_trans prod_lepoll_self eqpoll_imp_lepoll 
                  prod_commute_eqpoll) 
 
 lemma nat_lepoll_lemma:
      "\<lbrakk>0 \<notin> A; B \<in> A\<rbrakk> \<Longrightarrow> nat \<lesssim> ((nat \<rightarrow> \<Union>(A)) \<times> B) \<times> nat"
 by (blast dest: Sigma_fun_space_not0 intro: snd_lepoll_SigmaI)
 
 lemma AC9_AC1_lemma1:
      "\<lbrakk>0\<notin>A;  A\<noteq>0;   
          C = {((nat->\<Union>(A))*B)*nat. B \<in> A}  \<union>  
              {cons(0,((nat->\<Union>(A))*B)*nat). B \<in> A};  
          B1 \<in> C;  B2 \<in> C\<rbrakk>   
       \<Longrightarrow> B1 \<approx> B2"
 by (blast intro!: nat_lepoll_lemma Sigma_fun_space_eqpoll
                      nat_cons_eqpoll [THEN eqpoll_trans] 
                      prod_eqpoll_cong [OF _ eqpoll_refl]
              intro: eqpoll_trans eqpoll_sym )
 
 lemma AC9_AC1_lemma2:
      "\<forall>B1 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.   
       \<forall>B2 \<in> {(F*B)*N. B \<in> A} \<union> {cons(0,(F*B)*N). B \<in> A}.   
         f`\<langle>B1,B2\<rangle> \<in> bij(B1, B2)   
       \<Longrightarrow> (\<lambda>B \<in> A. snd(fst((f`<cons(0,(F*B)*N),(F*B)*N>)`0))) \<in> (\<Prod>X \<in> A. X)"
 apply (intro lam_type snd_type fst_type)
 apply (rule apply_type [OF _ consI1]) 
 apply (fast intro!: fun_weaken_type bij_is_fun)
 done
 
 lemma AC9_AC1: "AC9 \<Longrightarrow> AC1"
   unfolding AC1_def AC9_def
 apply (intro allI impI)
 apply (erule allE)
 apply (case_tac "A\<noteq>0")
 apply (blast dest: AC9_AC1_lemma1 AC9_AC1_lemma2, force) 
 done
 
 end
diff --git a/src/ZF/AC/WO1_WO7.thy b/src/ZF/AC/WO1_WO7.thy
--- a/src/ZF/AC/WO1_WO7.thy
+++ b/src/ZF/AC/WO1_WO7.thy
@@ -1,114 +1,114 @@
 (*  Title:      ZF/AC/WO1_WO7.thy
     Author:     Lawrence C Paulson, CU Computer Laboratory
     Copyright   1998  University of Cambridge
 
-WO7 \<longleftrightarrow> LEMMA \<longleftrightarrow> WO1 (Rubin \<and> Rubin p. 5)
+WO7 \<longleftrightarrow> LEMMA \<longleftrightarrow> WO1 (Rubin & Rubin p. 5)
 LEMMA is the sentence denoted by (**)
 
 Also, WO1 \<longleftrightarrow> WO8
 *)
 
 theory WO1_WO7
 imports AC_Equiv
 begin
 
 definition
     "LEMMA \<equiv>
      \<forall>X. \<not>Finite(X) \<longrightarrow> (\<exists>R. well_ord(X,R) \<and> \<not>well_ord(X,converse(R)))"
 
 (* ********************************************************************** *)
 (* It is easy to see that WO7 is equivalent to (**)                       *)
 (* ********************************************************************** *)
 
 lemma WO7_iff_LEMMA: "WO7 \<longleftrightarrow> LEMMA"
   unfolding WO7_def LEMMA_def
 apply (blast intro: Finite_well_ord_converse)
 done
 
 (* ********************************************************************** *)
 (* It is also easy to show that LEMMA implies WO1.                        *)
 (* ********************************************************************** *)
 
 lemma LEMMA_imp_WO1: "LEMMA \<Longrightarrow> WO1"
   unfolding WO1_def LEMMA_def Finite_def eqpoll_def
 apply (blast intro!: well_ord_rvimage [OF bij_is_inj nat_implies_well_ord])
 done
 
 (* ********************************************************************** *)
 (* The Rubins' proof of the other implication is contained within the     *)
 (* following sentence \<in>                                                   *)
 (* "... each infinite ordinal is well ordered by < but not by >."         *)
 (* This statement can be proved by the following two theorems.            *)
 (* But moreover we need to show similar property for any well ordered     *)
 (* infinite set. It is not very difficult thanks to Isabelle order types  *)
 (* We show that if a set is well ordered by some relation and by its     *)
 (* converse, then apropriate order type is well ordered by the converse   *)
 (* of it's membership relation, which in connection with the previous     *)
 (* gives the conclusion.                                                  *)
 (* ********************************************************************** *)
 
 lemma converse_Memrel_not_wf_on: 
     "\<lbrakk>Ord(a); \<not>Finite(a)\<rbrakk> \<Longrightarrow> \<not>wf[a](converse(Memrel(a)))"
   unfolding wf_on_def wf_def
 apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
 apply (rule notI)
 apply (erule_tac x = nat in allE, blast)
 done
 
 lemma converse_Memrel_not_well_ord: 
     "\<lbrakk>Ord(a); \<not>Finite(a)\<rbrakk> \<Longrightarrow> \<not>well_ord(a,converse(Memrel(a)))"
   unfolding well_ord_def
 apply (blast dest: converse_Memrel_not_wf_on)
 done
 
 lemma well_ord_rvimage_ordertype:
      "well_ord(A,r) \<Longrightarrow>
        rvimage (ordertype(A,r), converse(ordermap(A,r)),r) =
        Memrel(ordertype(A,r))" 
 by (blast intro: ordertype_ord_iso [THEN ord_iso_sym] ord_iso_rvimage_eq
              Memrel_type [THEN subset_Int_iff [THEN iffD1]] trans)
 
 lemma well_ord_converse_Memrel:
      "\<lbrakk>well_ord(A,r); well_ord(A,converse(r))\<rbrakk>   
       \<Longrightarrow> well_ord(ordertype(A,r), converse(Memrel(ordertype(A,r))))" 
 apply (subst well_ord_rvimage_ordertype [symmetric], assumption) 
 apply (rule rvimage_converse [THEN subst])
 apply (blast intro: ordertype_ord_iso ord_iso_sym ord_iso_is_bij
                     bij_is_inj well_ord_rvimage)
 done
 
 lemma WO1_imp_LEMMA: "WO1 \<Longrightarrow> LEMMA"
 apply (unfold WO1_def LEMMA_def, clarify) 
 apply (blast dest: well_ord_converse_Memrel
                    Ord_ordertype [THEN converse_Memrel_not_well_ord]
              intro: ordertype_ord_iso ord_iso_is_bij bij_is_inj lepoll_Finite
                     lepoll_def [THEN def_imp_iff, THEN iffD2] )
 done
 
 lemma WO1_iff_WO7: "WO1 \<longleftrightarrow> WO7"
 apply (simp add: WO7_iff_LEMMA)
 apply (blast intro: LEMMA_imp_WO1 WO1_imp_LEMMA)
 done
 
 
 
 (* ********************************************************************** *)
-(*            The proof of WO8 \<longleftrightarrow> WO1 (Rubin \<and> Rubin p. 6)               *)
+(*            The proof of WO8 \<longleftrightarrow> WO1 (Rubin & Rubin p. 6)               *)
 (* ********************************************************************** *)
 
 lemma WO1_WO8: "WO1 \<Longrightarrow> WO8"
 by (unfold WO1_def WO8_def, fast)
 
 
-(* The implication "WO8 \<Longrightarrow> WO1": a faithful image of Rubin \<and> Rubin's proof*)
+(* The implication "WO8 \<Longrightarrow> WO1": a faithful image of Rubin & Rubin's proof*)
 lemma WO8_WO1: "WO8 \<Longrightarrow> WO1"
   unfolding WO1_def WO8_def
 apply (rule allI)
 apply (erule_tac x = "{{x}. x \<in> A}" in allE)
 apply (erule impE)
  apply (rule_tac x = "\<lambda>a \<in> {{x}. x \<in> A}. THE x. a={x}" in exI)
  apply (force intro!: lam_type simp add: singleton_eq_iff the_equality)
 apply (blast intro: lam_sing_bij bij_is_inj well_ord_rvimage)
 done
 
 end
diff --git a/src/ZF/AC/WO2_AC16.thy b/src/ZF/AC/WO2_AC16.thy
--- a/src/ZF/AC/WO2_AC16.thy
+++ b/src/ZF/AC/WO2_AC16.thy
@@ -1,579 +1,579 @@
 (*  Title:      ZF/AC/WO2_AC16.thy
     Author:     Krzysztof Grabczewski
 
 The proof of WO2 \<Longrightarrow> AC16(k #+ m, k)
   
 The main part of the proof is the inductive reasoning concerning
 properties of constructed family T_gamma.
 The proof deals with three cases for ordinals: 0, succ and limit ordinal.
 The first instance is trivial, the third not difficult, but the second
 is very complicated requiring many lemmas.
 We also need to prove that at any stage gamma the set 
-(s - \<Union>(...) - k_gamma)   (Rubin \<and> Rubin page 15)
+(s - \<Union>(...) - k_gamma)   (Rubin & Rubin page 15)
 contains m distinct elements (in fact is equipollent to s)
 *)
 
 theory WO2_AC16 imports AC_Equiv AC16_lemmas Cardinal_aux begin
 
 (**** A recursive definition used in the proof of WO2 \<Longrightarrow> AC16 ****)
 
 definition
   recfunAC16 :: "[i,i,i,i] \<Rightarrow> i"  where
     "recfunAC16(f,h,i,a) \<equiv> 
          transrec2(i, 0, 
               \<lambda>g r. if (\<exists>y \<in> r. h`g \<subseteq> y) then r
                     else r \<union> {f`(\<mu> i. h`g \<subseteq> f`i \<and> 
                          (\<forall>b<a. (h`b \<subseteq> f`i \<longrightarrow> (\<forall>t \<in> r. \<not> h`b \<subseteq> t))))})"
 
 (* ********************************************************************** *)
 (* Basic properties of recfunAC16                                         *)
 (* ********************************************************************** *)
 
 lemma recfunAC16_0: "recfunAC16(f,h,0,a) = 0"
 by (simp add: recfunAC16_def)
 
 lemma recfunAC16_succ: 
      "recfunAC16(f,h,succ(i),a) =   
       (if (\<exists>y \<in> recfunAC16(f,h,i,a). h ` i \<subseteq> y) then recfunAC16(f,h,i,a)  
        else recfunAC16(f,h,i,a) \<union>  
             {f ` (\<mu> j. h ` i \<subseteq> f ` j \<and>   
              (\<forall>b<a. (h`b \<subseteq> f`j   
               \<longrightarrow> (\<forall>t \<in> recfunAC16(f,h,i,a). \<not> h`b \<subseteq> t))))})"
 apply (simp add: recfunAC16_def)
 done
 
 lemma recfunAC16_Limit: "Limit(i)   
         \<Longrightarrow> recfunAC16(f,h,i,a) = (\<Union>j<i. recfunAC16(f,h,j,a))"
 by (simp add: recfunAC16_def transrec2_Limit)
 
 (* ********************************************************************** *)
 (* Monotonicity of transrec2                                              *)
 (* ********************************************************************** *)
 
 lemma transrec2_mono_lemma [rule_format]:
      "\<lbrakk>\<And>g r. r \<subseteq> B(g,r);  Ord(i)\<rbrakk>   
       \<Longrightarrow> j<i \<longrightarrow> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
 apply (erule trans_induct)
 apply (rule Ord_cases, assumption+, fast)
 apply (simp (no_asm_simp))
 apply (blast elim!: leE) 
 apply (simp add: transrec2_Limit) 
 apply (blast intro: OUN_I ltI Ord_in_Ord [THEN le_refl]
              elim!: Limit_has_succ [THEN ltE])
 done
 
 lemma transrec2_mono:
      "\<lbrakk>\<And>g r. r \<subseteq> B(g,r); j\<le>i\<rbrakk> 
       \<Longrightarrow> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
 apply (erule leE)
 apply (rule transrec2_mono_lemma)
 apply (auto intro: lt_Ord2 ) 
 done
 
 (* ********************************************************************** *)
 (* Monotonicity of recfunAC16                                             *)
 (* ********************************************************************** *)
 
 lemma recfunAC16_mono: 
        "i\<le>j \<Longrightarrow> recfunAC16(f, g, i, a) \<subseteq> recfunAC16(f, g, j, a)"
   unfolding recfunAC16_def
 apply (rule transrec2_mono, auto) 
 done
 
 (* ********************************************************************** *)
 (* case of limit ordinal                                                  *)
 (* ********************************************************************** *)
 
 
 lemma lemma3_1:
     "\<lbrakk>\<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) \<and> f(z)<=Y);
         \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); j\<le>i; i<x; z<a;
         V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W\<rbrakk>   
      \<Longrightarrow> V = W"
 apply (erule asm_rl allE impE)+
 apply (drule subsetD, assumption, blast) 
 done
 
 
 lemma lemma3:
     "\<lbrakk>\<forall>y<x. \<forall>z<a. z<y | (\<exists>Y \<in> F(y). f(z)<=Y) \<longrightarrow> (\<exists>! Y. Y \<in> F(y) \<and> f(z)<=Y);
         \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j); i<x; j<x; z<a;   
         V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W\<rbrakk>   
      \<Longrightarrow> V = W"
 apply (rule_tac j=j in Ord_linear_le [OF lt_Ord lt_Ord], assumption+)
 apply (erule lemma3_1 [symmetric], assumption+)
 apply (erule lemma3_1, assumption+)
 done
 
 lemma lemma4:
      "\<lbrakk>\<forall>y<x. F(y) \<subseteq> X \<and>   
                 (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow>   
                  (\<exists>! Y. Y \<in> F(y) \<and> h(x) \<subseteq> Y)); 
          x < a\<rbrakk>   
       \<Longrightarrow> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) \<longrightarrow>   
                        (\<exists>! Y. Y \<in> F(y) \<and> h(z) \<subseteq> Y)"
 apply (intro oallI impI)
 apply (drule ospec, assumption, clarify)
 apply (blast elim!: oallE ) 
 done
 
 lemma lemma5:
      "\<lbrakk>\<forall>y<x. F(y) \<subseteq> X \<and>   
                (\<forall>x<a. x < y | (\<exists>Y \<in> F(y). h(x) \<subseteq> Y) \<longrightarrow>   
                 (\<exists>! Y. Y \<in> F(y) \<and> h(x) \<subseteq> Y));  
          x < a; Limit(x); \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j)\<rbrakk>   
       \<Longrightarrow> (\<Union>x<x. F(x)) \<subseteq> X \<and>   
           (\<forall>xa<a. xa < x | (\<exists>x \<in> \<Union>x<x. F(x). h(xa) \<subseteq> x)   
                 \<longrightarrow> (\<exists>! Y. Y \<in> (\<Union>x<x. F(x)) \<and> h(xa) \<subseteq> Y))"
 apply (rule conjI)
 apply (rule subsetI)
 apply (erule OUN_E)
 apply (drule ospec, assumption, fast)
 apply (drule lemma4, assumption)
 apply (rule oallI)
 apply (rule impI)
 apply (erule disjE)
 apply (frule ospec, erule Limit_has_succ, assumption) 
 apply (drule_tac A = a and x = xa in ospec, assumption)
 apply (erule impE, rule le_refl [THEN disjI1], erule lt_Ord) 
 apply (blast intro: lemma3 Limit_has_succ) 
 apply (blast intro: lemma3) 
 done
 
 (* ********************************************************************** *)
 (* case of successor ordinal                                              *)
 (* ********************************************************************** *)
 
 (*
   First quite complicated proof of the fact used in the recursive construction
   of the family T_gamma (WO2 \<Longrightarrow> AC16(k #+ m, k)) - the fact that at any stage
   gamma the set (s - \<Union>(...) - k_gamma) is equipollent to s
-  (Rubin \<and> Rubin page 15).
+  (Rubin & Rubin page 15).
 *)
 
 (* ********************************************************************** *)
 (* dbl_Diff_eqpoll_Card                                                   *)
 (* ********************************************************************** *)
 
 
 lemma dbl_Diff_eqpoll_Card:
       "\<lbrakk>A\<approx>a; Card(a); \<not>Finite(a); B\<prec>a; C\<prec>a\<rbrakk> \<Longrightarrow> A - B - C\<approx>a"
 by (blast intro: Diff_lesspoll_eqpoll_Card) 
 
 (* ********************************************************************** *)
 (* Case of finite ordinals                                                *)
 (* ********************************************************************** *)
 
 
 lemma Finite_lesspoll_infinite_Ord: 
       "\<lbrakk>Finite(X); \<not>Finite(a); Ord(a)\<rbrakk> \<Longrightarrow> X\<prec>a"
   unfolding lesspoll_def
 apply (rule conjI)
 apply (drule nat_le_infinite_Ord [THEN le_imp_lepoll], assumption)
   unfolding Finite_def
 apply (blast intro: leI [THEN le_imp_subset, THEN subset_imp_lepoll]
                     ltI eqpoll_imp_lepoll lepoll_trans) 
 apply (blast intro: eqpoll_sym [THEN eqpoll_trans])
 done
 
 lemma Union_lesspoll:
      "\<lbrakk>\<forall>x \<in> X. x \<lesssim> n \<and> x \<subseteq> T; well_ord(T, R); X \<lesssim> b;   
          b<a; \<not>Finite(a); Card(a); n \<in> nat\<rbrakk>   
       \<Longrightarrow> \<Union>(X)\<prec>a"
 apply (case_tac "Finite (X)")
 apply (blast intro: Card_is_Ord Finite_lesspoll_infinite_Ord 
                     lepoll_nat_imp_Finite Finite_Union)
 apply (drule lepoll_imp_ex_le_eqpoll) 
 apply (erule lt_Ord) 
 apply (elim exE conjE)
 apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
 apply (erule eqpoll_sym [THEN eqpoll_def [THEN def_imp_iff, THEN iffD1],
                          THEN exE])
 apply (frule bij_is_surj [THEN surj_image_eq])
 apply (drule image_fun [OF bij_is_fun subset_refl])
 apply (drule sym [THEN trans], assumption)
 apply (blast intro: lt_Ord UN_lepoll lt_Card_imp_lesspoll
                     lt_trans1 lesspoll_trans1)
 done
 
 (* ********************************************************************** *)
 (* recfunAC16_lepoll_index                                                *)
 (* ********************************************************************** *)
 
 lemma Un_sing_eq_cons: "A \<union> {a} = cons(a, A)"
 by fast
 
 lemma Un_lepoll_succ: "A \<lesssim> B \<Longrightarrow> A \<union> {a} \<lesssim> succ(B)"
 apply (simp add: Un_sing_eq_cons succ_def)
 apply (blast elim!: mem_irrefl intro: cons_lepoll_cong)
 done
 
 lemma Diff_UN_succ_empty: "Ord(a) \<Longrightarrow> F(a) - (\<Union>b<succ(a). F(b)) = 0"
 by (fast intro!: le_refl)
 
 lemma Diff_UN_succ_subset: "Ord(a) \<Longrightarrow> F(a) \<union> X - (\<Union>b<succ(a). F(b)) \<subseteq> X"
 by blast
 
 lemma recfunAC16_Diff_lepoll_1:
      "Ord(x) 
       \<Longrightarrow> recfunAC16(f, g, x, a) - (\<Union>i<x. recfunAC16(f, g, i, a)) \<lesssim> 1"
 apply (erule Ord_cases)
   apply (simp add: recfunAC16_0 empty_subsetI [THEN subset_imp_lepoll])
 (*Limit case*)
 prefer 2 apply (simp add: recfunAC16_Limit Diff_cancel 
                           empty_subsetI [THEN subset_imp_lepoll])
 (*succ case*)
 apply (simp add: recfunAC16_succ
                  Diff_UN_succ_empty [of _ "\<lambda>j. recfunAC16(f,g,j,a)"]
                  empty_subsetI [THEN subset_imp_lepoll])
 apply (best intro: Diff_UN_succ_subset [THEN subset_imp_lepoll]
                    singleton_eqpoll_1 [THEN eqpoll_imp_lepoll] lepoll_trans)
 done
 
 lemma in_Least_Diff:
      "\<lbrakk>z \<in> F(x); Ord(x)\<rbrakk>   
       \<Longrightarrow> z \<in> F(\<mu> i. z \<in> F(i)) - (\<Union>j<(\<mu> i. z \<in> F(i)). F(j))"
 by (fast elim: less_LeastE elim!: LeastI)
 
 lemma Least_eq_imp_ex:
      "\<lbrakk>(\<mu> i. w \<in> F(i)) = (\<mu> i. z \<in> F(i));   
          w \<in> (\<Union>i<a. F(i)); z \<in> (\<Union>i<a. F(i))\<rbrakk>   
       \<Longrightarrow> \<exists>b<a. w \<in> (F(b) - (\<Union>c<b. F(c))) \<and> z \<in> (F(b) - (\<Union>c<b. F(c)))"
 apply (elim OUN_E)
 apply (drule in_Least_Diff, erule lt_Ord) 
 apply (frule in_Least_Diff, erule lt_Ord) 
 apply (rule oexI, force) 
 apply (blast intro: lt_Ord Least_le [THEN lt_trans1]) 
 done
 
 
 lemma two_in_lepoll_1: "\<lbrakk>A \<lesssim> 1; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> a=b"
 by (fast dest!: lepoll_1_is_sing)
 
 
 lemma UN_lepoll_index:
      "\<lbrakk>\<forall>i<a. F(i)-(\<Union>j<i. F(j)) \<lesssim> 1; Limit(a)\<rbrakk>   
       \<Longrightarrow> (\<Union>x<a. F(x)) \<lesssim> a"
 apply (rule lepoll_def [THEN def_imp_iff [THEN iffD2]])
 apply (rule_tac x = "\<lambda>z \<in> (\<Union>x<a. F (x)). \<mu> i. z \<in> F (i) " in exI)
   unfolding inj_def
 apply (rule CollectI)
 apply (rule lam_type)
 apply (erule OUN_E)
 apply (erule Least_in_Ord)
 apply (erule ltD)
 apply (erule lt_Ord2)
 apply (intro ballI)
 apply (simp (no_asm_simp))
 apply (rule impI)
 apply (drule Least_eq_imp_ex, assumption+)
 apply (fast elim!: two_in_lepoll_1)
 done
 
 
 lemma recfunAC16_lepoll_index: "Ord(y) \<Longrightarrow> recfunAC16(f, h, y, a) \<lesssim> y"
 apply (erule trans_induct3)
 (*0 case*)
 apply (simp (no_asm_simp) add: recfunAC16_0 lepoll_refl)
 (*succ case*)
 apply (simp (no_asm_simp) add: recfunAC16_succ)
 apply (blast dest!: succI1 [THEN rev_bspec] 
              intro: subset_succI [THEN subset_imp_lepoll] Un_lepoll_succ  
                     lepoll_trans)
 apply (simp (no_asm_simp) add: recfunAC16_Limit)
 apply (blast intro: lt_Ord [THEN recfunAC16_Diff_lepoll_1] UN_lepoll_index)
 done
 
 
 lemma Union_recfunAC16_lesspoll:
      "\<lbrakk>recfunAC16(f,g,y,a) \<subseteq> {X \<in> Pow(A). X\<approx>n};   
          A\<approx>a;  y<a;  \<not>Finite(a);  Card(a);  n \<in> nat\<rbrakk>   
       \<Longrightarrow> \<Union>(recfunAC16(f,g,y,a))\<prec>a"
 apply (erule eqpoll_def [THEN def_imp_iff, THEN iffD1, THEN exE])
 apply (rule_tac T=A in Union_lesspoll, simp_all)
 apply (blast intro!: eqpoll_imp_lepoll)
 apply (blast intro: bij_is_inj Card_is_Ord [THEN well_ord_Memrel]
                     well_ord_rvimage)
 apply (erule lt_Ord [THEN recfunAC16_lepoll_index])
 done
 
 lemma dbl_Diff_eqpoll:
      "\<lbrakk>recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)};   
          Card(a); \<not> Finite(a); A\<approx>a;   
          k \<in> nat;  y<a;   
          h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)})\<rbrakk>   
       \<Longrightarrow> A - \<Union>(recfunAC16(f, h, y, a)) - h`y\<approx>a"
 apply (rule dbl_Diff_eqpoll_Card, simp_all)
 apply (simp add: Union_recfunAC16_lesspoll)
 apply (rule Finite_lesspoll_infinite_Ord) 
 apply (rule Finite_def [THEN def_imp_iff, THEN iffD2]) 
 apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption)  
 apply (blast intro: Card_is_Ord) 
 done
 
 (* back to the proof *)
 
 lemmas disj_Un_eqpoll_nat_sum = 
     eqpoll_trans [THEN eqpoll_trans, 
                   OF disj_Un_eqpoll_sum sum_eqpoll_cong nat_sum_eqpoll_sum]
 
 
 lemma Un_in_Collect: "\<lbrakk>x \<in> Pow(A - B - h`i); x\<approx>m;   
         h \<in> bij(a, {x \<in> Pow(A) . x\<approx>k}); i<a; k \<in> nat; m \<in> nat\<rbrakk>   
         \<Longrightarrow> h ` i \<union> x \<in> {x \<in> Pow(A) . x\<approx>k #+ m}"
 by (blast intro: disj_Un_eqpoll_nat_sum
           dest:  ltD bij_is_fun [THEN apply_type])
 
 
 (* ********************************************************************** *)
 (* Lemmas simplifying assumptions                                         *)
 (* ********************************************************************** *)
 
 lemma lemma6:
      "\<lbrakk>\<forall>y<succ(j). F(y)<=X \<and> (\<forall>x<a. x<y | P(x,y) \<longrightarrow> Q(x,y)); succ(j)<a\<rbrakk>
       \<Longrightarrow> F(j)<=X \<and> (\<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j))"
 by (blast intro!: lt_Ord succI1 [THEN ltI, THEN lt_Ord, THEN le_refl]) 
 
 
 lemma lemma7:
      "\<lbrakk>\<forall>x<a. x<j | P(x,j) \<longrightarrow> Q(x,j);  succ(j)<a\<rbrakk>   
       \<Longrightarrow> P(j,j) \<longrightarrow> (\<forall>x<a. x\<le>j | P(x,j) \<longrightarrow> Q(x,j))"
 by (fast elim!: leE)
 
 (* ********************************************************************** *)
 (* Lemmas needed to prove ex_next_set, which means that for any successor *)
 (* ordinal there is a set satisfying certain properties                   *)
 (* ********************************************************************** *)
 
 lemma ex_subset_eqpoll:
      "\<lbrakk>A\<approx>a; \<not> Finite(a); Ord(a); m \<in> nat\<rbrakk> \<Longrightarrow> \<exists>X \<in> Pow(A). X\<approx>m"
 apply (rule lepoll_imp_eqpoll_subset [of m A, THEN exE]) 
  apply (rule lepoll_trans, rule leI [THEN le_imp_lepoll])
   apply (blast intro: lt_trans2 [OF ltI nat_le_infinite_Ord] Ord_nat)
 apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) 
 apply (fast elim!: eqpoll_sym)
 done
 
 lemma subset_Un_disjoint: "\<lbrakk>A \<subseteq> B \<union> C; A \<inter> C = 0\<rbrakk> \<Longrightarrow> A \<subseteq> B"
 by blast
 
 
 lemma Int_empty:
      "\<lbrakk>X \<in> Pow(A - \<Union>(B) -C); T \<in> B; F \<subseteq> T\<rbrakk> \<Longrightarrow> F \<inter> X = 0"
 by blast
 
 
 (* ********************************************************************** *)
 (* equipollent subset (and finite) is the whole set                       *)
 (* ********************************************************************** *)
 
 
 lemma subset_imp_eq_lemma:
      "m \<in> nat \<Longrightarrow> \<forall>A B. A \<subseteq> B \<and> m \<lesssim> A \<and> B \<lesssim> m \<longrightarrow> A=B"
 apply (induct_tac "m")
 apply (fast dest!: lepoll_0_is_0)
 apply (intro allI impI)
 apply (elim conjE)
 apply (rule succ_lepoll_imp_not_empty [THEN not_emptyE], assumption)
 apply (frule subsetD [THEN Diff_sing_lepoll], assumption+)
 apply (frule lepoll_Diff_sing)
 apply (erule allE impE)+
 apply (rule conjI)
 prefer 2 apply fast
 apply fast
 apply (blast elim: equalityE) 
 done
 
 
 lemma subset_imp_eq: "\<lbrakk>A \<subseteq> B; m \<lesssim> A; B \<lesssim> m; m \<in> nat\<rbrakk> \<Longrightarrow> A=B"
 by (blast dest!: subset_imp_eq_lemma)
 
 
 lemma bij_imp_arg_eq:
      "\<lbrakk>f \<in> bij(a, {Y \<in> X. Y\<approx>succ(k)}); k \<in> nat; f`b \<subseteq> f`y; b<a; y<a\<rbrakk> 
       \<Longrightarrow> b=y"
 apply (drule subset_imp_eq)
 apply (erule_tac [3] nat_succI)
   unfolding bij_def inj_def
 apply (blast intro: eqpoll_sym eqpoll_imp_lepoll
              dest:  ltD apply_type)+
 done
 
 
 lemma ex_next_set:
      "\<lbrakk>recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)};   
          Card(a); \<not> Finite(a); A\<approx>a;   
          k \<in> nat; m \<in> nat; y<a;   
          h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)});   
          \<not> (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y)\<rbrakk>   
       \<Longrightarrow> \<exists>X \<in> {Y \<in> Pow(A). Y\<approx>succ(k #+ m)}. h`y \<subseteq> X \<and>   
                 (\<forall>b<a. h`b \<subseteq> X \<longrightarrow>   
                 (\<forall>T \<in> recfunAC16(f, h, y, a). \<not> h`b \<subseteq> T))"
 apply (erule_tac m1=m in dbl_Diff_eqpoll [THEN ex_subset_eqpoll, THEN bexE], 
        assumption+)
 apply (erule Card_is_Ord, assumption)
 apply (frule Un_in_Collect, (erule asm_rl nat_succI)+) 
 apply (erule CollectE)
 apply (rule rev_bexI, simp)
 apply (rule conjI, blast) 
 apply (intro ballI impI oallI notI)
 apply (drule subset_Un_disjoint, rule Int_empty, assumption+)
 apply (blast dest: bij_imp_arg_eq) 
 done
 
 (* ********************************************************************** *)
 (* Lemma ex_next_Ord states that for any successor                        *)
 (* ordinal there is a number of the set satisfying certain properties     *)
 (* ********************************************************************** *)
 
 lemma ex_next_Ord:
      "\<lbrakk>recfunAC16(f, h, y, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)};   
          Card(a); \<not> Finite(a); A\<approx>a;   
          k \<in> nat; m \<in> nat; y<a;   
          h \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k)});   
          f \<in> bij(a, {Y \<in> Pow(A). Y\<approx>succ(k #+ m)});   
          \<not> (\<exists>Y \<in> recfunAC16(f, h, y, a). h`y \<subseteq> Y)\<rbrakk>   
       \<Longrightarrow> \<exists>c<a. h`y \<subseteq> f`c \<and>   
                 (\<forall>b<a. h`b \<subseteq> f`c \<longrightarrow>   
                 (\<forall>T \<in> recfunAC16(f, h, y, a). \<not> h`b \<subseteq> T))"
 apply (drule ex_next_set, assumption+)
 apply (erule bexE)
 apply (rule_tac x="converse(f)`X" in oexI)
 apply (simp add: right_inverse_bij)
 apply (blast intro: bij_converse_bij bij_is_fun [THEN apply_type] ltI
                     Card_is_Ord)
 done
 
 
 (* ********************************************************************** *)
 (* Lemma simplifying assumptions                                          *)
 (* ********************************************************************** *)
 
 lemma lemma8:
      "\<lbrakk>\<forall>x<a. x<j | (\<exists>xa \<in> F(j). P(x, xa))   
          \<longrightarrow> (\<exists>! Y. Y \<in> F(j) \<and> P(x, Y)); F(j) \<subseteq> X;   
          L \<in> X; P(j, L) \<and> (\<forall>x<a. P(x, L) \<longrightarrow> (\<forall>xa \<in> F(j). \<not>P(x, xa)))\<rbrakk>   
       \<Longrightarrow> F(j) \<union> {L} \<subseteq> X \<and>   
           (\<forall>x<a. x\<le>j | (\<exists>xa \<in> (F(j) \<union> {L}). P(x, xa)) \<longrightarrow>   
                  (\<exists>! Y. Y \<in> (F(j) \<union> {L}) \<and> P(x, Y)))"
 apply (rule conjI)
 apply (fast intro!: singleton_subsetI)
 apply (rule oallI)
 apply (blast elim!: leE oallE)
 done
 
 (* ********************************************************************** *)
 (* The main part of the proof: inductive proof of the property of T_gamma *)
 (* lemma main_induct                                                      *)
 (* ********************************************************************** *)
 
 lemma main_induct:
      "\<lbrakk>b < a; f \<in> bij(a, {Y \<in> Pow(A) . Y\<approx>succ(k #+ m)});   
          h \<in> bij(a, {Y \<in> Pow(A) . Y\<approx>succ(k)});   
          \<not>Finite(a); Card(a); A\<approx>a; k \<in> nat; m \<in> nat\<rbrakk>   
       \<Longrightarrow> recfunAC16(f, h, b, a) \<subseteq> {X \<in> Pow(A) . X\<approx>succ(k #+ m)} \<and>   
           (\<forall>x<a. x < b | (\<exists>Y \<in> recfunAC16(f, h, b, a). h ` x \<subseteq> Y) \<longrightarrow>   
           (\<exists>! Y. Y \<in> recfunAC16(f, h, b, a) \<and> h ` x \<subseteq> Y))"
 apply (erule lt_induct)
 apply (frule lt_Ord)
 apply (erule Ord_cases)
 (* case 0 *)
 apply (simp add: recfunAC16_0)
 (* case Limit *)
 prefer 2  apply (simp add: recfunAC16_Limit)
           apply (rule lemma5, assumption+)
           apply (blast dest!: recfunAC16_mono)
 (* case succ *)
 apply clarify 
 apply (erule lemma6 [THEN conjE], assumption)
 apply (simp (no_asm_simp) split del: split_if add: recfunAC16_succ)
 apply (rule conjI [THEN split_if [THEN iffD2]])
  apply (simp, erule lemma7, assumption)
 apply (rule impI)
 apply (rule ex_next_Ord [THEN oexE], 
        assumption+, rule le_refl [THEN lt_trans], assumption+) 
 apply (erule lemma8, assumption)
  apply (rule bij_is_fun [THEN apply_type], assumption)
  apply (erule Least_le [THEN lt_trans2, THEN ltD])
   apply (erule lt_Ord) 
  apply (erule succ_leI)
 apply (erule LeastI) 
 apply (erule lt_Ord) 
 done
 
 (* ********************************************************************** *)
 (* Lemma to simplify the inductive proof                                  *)
 (*   - the desired property is a consequence of the inductive assumption  *)
 (* ********************************************************************** *)
 
 lemma lemma_simp_induct:
      "\<lbrakk>\<forall>b. b<a \<longrightarrow> F(b) \<subseteq> S \<and> (\<forall>x<a. (x<b | (\<exists>Y \<in> F(b). f`x \<subseteq> Y))  
                                    \<longrightarrow> (\<exists>! Y. Y \<in> F(b) \<and> f`x \<subseteq> Y));
          f \<in> a->f``(a); Limit(a); 
          \<forall>i j. i\<le>j \<longrightarrow> F(i) \<subseteq> F(j)\<rbrakk>   
         \<Longrightarrow> (\<Union>j<a. F(j)) \<subseteq> S \<and>   
             (\<forall>x \<in> f``a. \<exists>! Y. Y \<in> (\<Union>j<a. F(j)) \<and> x \<subseteq> Y)"
 apply (rule conjI)
 apply (rule subsetI)
 apply (erule OUN_E, blast) 
 apply (rule ballI)
 apply (erule imageE)
 apply (drule ltI, erule Limit_is_Ord) 
 apply (drule Limit_has_succ, assumption) 
 apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption)
 apply (erule conjE)
 apply (drule ospec) 
 (** LEVEL 10 **)
 apply (erule leI [THEN succ_leE])
 apply (erule impE)
 apply (fast elim!: leI [THEN succ_leE, THEN lt_Ord, THEN le_refl])
 apply (drule apply_equality, assumption) 
 apply (elim conjE ex1E)
 (** LEVEL 15 **)
 apply (rule ex1I, blast) 
 apply (elim conjE OUN_E)
 apply (erule_tac i="succ(xa)" and j=aa 
        in Ord_linear_le [OF lt_Ord lt_Ord], assumption)
 prefer 2 
 apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 
 (** LEVEL 20 **)
 apply (drule_tac x1=aa in spec [THEN mp], assumption)
 apply (frule succ_leE)
 apply (drule spec [THEN spec, THEN mp, THEN subsetD], assumption+, blast) 
 done
 
 (* ********************************************************************** *)
 (* The target theorem                                                     *)
 (* ********************************************************************** *)
 
 theorem WO2_AC16: "\<lbrakk>WO2; 0<m; k \<in> nat; m \<in> nat\<rbrakk> \<Longrightarrow> AC16(k #+ m,k)"
   unfolding AC16_def
 apply (rule allI)
 apply (rule impI)
 apply (frule WO2_infinite_subsets_eqpoll_X, assumption+)
 apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp, simp) 
 apply (frule WO2_imp_ex_Card)
 apply (elim exE conjE)
 apply (drule eqpoll_trans [THEN eqpoll_sym, 
                            THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]],
        assumption)
 apply (drule eqpoll_trans [THEN eqpoll_sym, 
                            THEN eqpoll_def [THEN def_imp_iff, THEN iffD1]], 
        assumption+)
 apply (elim exE)
 apply (rename_tac h)
 apply (rule_tac x = "\<Union>j<a. recfunAC16 (h,f,j,a) " in exI)
 apply (rule_tac P="\<lambda>z. Y \<and> (\<forall>x \<in> z. Z(x))"  for Y Z
        in bij_is_surj [THEN surj_image_eq, THEN subst], assumption)
 apply (rule lemma_simp_induct)
 apply (blast del: conjI notI
              intro!: main_induct eqpoll_imp_lepoll [THEN lepoll_infinite] ) 
 apply (blast intro: bij_is_fun [THEN surj_image, THEN surj_is_fun])
 apply (erule eqpoll_imp_lepoll [THEN lepoll_infinite, 
                                 THEN infinite_Card_is_InfCard, 
                                 THEN InfCard_is_Limit], 
        assumption+)
 apply (blast dest!: recfunAC16_mono)
 done
 
 end
diff --git a/src/ZF/AC/WO6_WO1.thy b/src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy
+++ b/src/ZF/AC/WO6_WO1.thy
@@ -1,539 +1,539 @@
 (*  Title:      ZF/AC/WO6_WO1.thy
     Author:     Krzysztof Grabczewski
 
 Proofs needed to state that formulations WO1,...,WO6 are all equivalent.
 The only hard one is WO6 \<Longrightarrow> WO1.
 
 Every proof (except WO6 \<Longrightarrow> WO1 and WO1 \<Longrightarrow> WO2) are described as "clear"
-by Rubin \<and> Rubin (page 2). 
+by Rubin & Rubin (page 2). 
 They refer reader to a book by Gödel to see the proof WO1 \<Longrightarrow> WO2.
 Fortunately order types made this proof also very easy.
 *)
 
 theory WO6_WO1
 imports Cardinal_aux
 begin
 
 (* Auxiliary definitions used in proof *)
 definition
   NN  :: "i \<Rightarrow> i"  where
     "NN(y) \<equiv> {m \<in> nat. \<exists>a. \<exists>f. Ord(a) \<and> domain(f)=a  \<and>  
                         (\<Union>b<a. f`b) = y \<and> (\<forall>b<a. f`b \<lesssim> m)}"
   
 definition
   uu  :: "[i, i, i, i] \<Rightarrow> i"  where
     "uu(f, beta, gamma, delta) \<equiv> (f`beta * f`gamma) \<inter> f`delta"
 
 
 (** Definitions for case 1 **)
 definition
   vv1 :: "[i, i, i] \<Rightarrow> i"  where
      "vv1(f,m,b) \<equiv>                                                
            let g = \<mu> g. (\<exists>d. Ord(d) \<and> (domain(uu(f,b,g,d)) \<noteq> 0 \<and> 
                                  domain(uu(f,b,g,d)) \<lesssim> m));      
                d = \<mu> d. domain(uu(f,b,g,d)) \<noteq> 0 \<and>                  
                             domain(uu(f,b,g,d)) \<lesssim> m         
            in  if f`b \<noteq> 0 then domain(uu(f,b,g,d)) else 0"
 
 definition
   ww1 :: "[i, i, i] \<Rightarrow> i"  where
      "ww1(f,m,b) \<equiv> f`b - vv1(f,m,b)"
 
 definition
   gg1 :: "[i, i, i] \<Rightarrow> i"  where
      "gg1(f,a,m) \<equiv> \<lambda>b \<in> a++a. if b<a then vv1(f,m,b) else ww1(f,m,b--a)"
 
 
 (** Definitions for case 2 **)
 definition
   vv2 :: "[i, i, i, i] \<Rightarrow> i"  where
      "vv2(f,b,g,s) \<equiv>   
            if f`g \<noteq> 0 then {uu(f, b, g, \<mu> d. uu(f,b,g,d) \<noteq> 0)`s} else 0"
 
 definition
   ww2 :: "[i, i, i, i] \<Rightarrow> i"  where
      "ww2(f,b,g,s) \<equiv> f`g - vv2(f,b,g,s)"
 
 definition
   gg2 :: "[i, i, i, i] \<Rightarrow> i"  where
      "gg2(f,a,b,s) \<equiv>
               \<lambda>g \<in> a++a. if g<a then vv2(f,b,g,s) else ww2(f,b,g--a,s)"
 
 
 lemma WO2_WO3: "WO2 \<Longrightarrow> WO3"
 by (unfold WO2_def WO3_def, fast)
 
 (* ********************************************************************** *)
 
 lemma WO3_WO1: "WO3 \<Longrightarrow> WO1"
   unfolding eqpoll_def WO1_def WO3_def
 apply (intro allI)
 apply (drule_tac x=A in spec) 
 apply (blast intro: bij_is_inj well_ord_rvimage 
                     well_ord_Memrel [THEN well_ord_subset])
 done
 
 (* ********************************************************************** *)
 
 lemma WO1_WO2: "WO1 \<Longrightarrow> WO2"
   unfolding eqpoll_def WO1_def WO2_def
 apply (blast intro!: Ord_ordertype ordermap_bij)
 done
 
 (* ********************************************************************** *)
 
 lemma lam_sets: "f \<in> A->B \<Longrightarrow> (\<lambda>x \<in> A. {f`x}): A -> {{b}. b \<in> B}"
 by (fast intro!: lam_type apply_type)
 
 lemma surj_imp_eq': "f \<in> surj(A,B) \<Longrightarrow> (\<Union>a \<in> A. {f`a}) = B"
   unfolding surj_def
 apply (fast elim!: apply_type)
 done
 
 lemma surj_imp_eq: "\<lbrakk>f \<in> surj(A,B); Ord(A)\<rbrakk> \<Longrightarrow> (\<Union>a<A. {f`a}) = B"
 by (fast dest!: surj_imp_eq' intro!: ltI elim!: ltE)
 
 lemma WO1_WO4: "WO1 \<Longrightarrow> WO4(1)"
   unfolding WO1_def WO4_def
 apply (rule allI)
 apply (erule_tac x = A in allE)
 apply (erule exE)
 apply (intro exI conjI)
 apply (erule Ord_ordertype)
 apply (erule ordermap_bij [THEN bij_converse_bij, THEN bij_is_fun, THEN lam_sets, THEN domain_of_fun])
 apply (simp_all add: singleton_eqpoll_1 eqpoll_imp_lepoll Ord_ordertype
        ordermap_bij [THEN bij_converse_bij, THEN bij_is_surj, THEN surj_imp_eq]
        ltD)
 done
 
 (* ********************************************************************** *)
 
 lemma WO4_mono: "\<lbrakk>m\<le>n; WO4(m)\<rbrakk> \<Longrightarrow> WO4(n)"
   unfolding WO4_def
 apply (blast dest!: spec intro: lepoll_trans [OF _ le_imp_lepoll])
 done
 
 (* ********************************************************************** *)
 
 lemma WO4_WO5: "\<lbrakk>m \<in> nat; 1\<le>m; WO4(m)\<rbrakk> \<Longrightarrow> WO5"
 by (unfold WO4_def WO5_def, blast)
 
 (* ********************************************************************** *)
 
 lemma WO5_WO6: "WO5 \<Longrightarrow> WO6"
 by (unfold WO4_def WO5_def WO6_def, blast)
 
 
 (* ********************************************************************** 
     The proof of "WO6 \<Longrightarrow> WO1".  Simplified by L C Paulson.
 
-    From the book "Equivalents of the Axiom of Choice" by Rubin \<and> Rubin,
+    From the book "Equivalents of the Axiom of Choice" by Rubin & Rubin,
     pages 2-5
 ************************************************************************* *)
 
 lemma lt_oadd_odiff_disj:
       "\<lbrakk>k < i++j;  Ord(i);  Ord(j)\<rbrakk> 
        \<Longrightarrow> k < i  |  (\<not> k<i \<and> k = i ++ (k--i) \<and> (k--i)<j)"
 apply (rule_tac i = k and j = i in Ord_linear2)
 prefer 4 
    apply (drule odiff_lt_mono2, assumption)
    apply (simp add: oadd_odiff_inverse odiff_oadd_inverse)
 apply (auto elim!: lt_Ord)
 done
 
 
 (* ********************************************************************** *)
 (* The most complicated part of the proof - lemma ii - p. 2-4             *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
 (* some properties of relation uu(beta, gamma, delta) - p. 2              *)
 (* ********************************************************************** *)
 
 lemma domain_uu_subset: "domain(uu(f,b,g,d)) \<subseteq> f`b"
 by (unfold uu_def, blast)
 
 lemma quant_domain_uu_lepoll_m:
      "\<forall>b<a. f`b \<lesssim> m \<Longrightarrow> \<forall>b<a. \<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<lesssim> m"
 by (blast intro: domain_uu_subset [THEN subset_imp_lepoll] lepoll_trans)
 
 lemma uu_subset1: "uu(f,b,g,d) \<subseteq> f`b * f`g"
 by (unfold uu_def, blast)
 
 lemma uu_subset2: "uu(f,b,g,d) \<subseteq> f`d"
 by (unfold uu_def, blast)
 
 lemma uu_lepoll_m: "\<lbrakk>\<forall>b<a. f`b \<lesssim> m;  d<a\<rbrakk> \<Longrightarrow> uu(f,b,g,d) \<lesssim> m"
 by (blast intro: uu_subset2 [THEN subset_imp_lepoll] lepoll_trans)
 
 (* ********************************************************************** *)
 (* Two cases for lemma ii                                                 *)
 (* ********************************************************************** *)
 lemma cases: 
      "\<forall>b<a. \<forall>g<a. \<forall>d<a. u(f,b,g,d) \<lesssim> m   
       \<Longrightarrow> (\<forall>b<a. f`b \<noteq> 0 \<longrightarrow>  
                   (\<exists>g<a. \<exists>d<a. u(f,b,g,d) \<noteq> 0 \<and> u(f,b,g,d) \<prec> m))  
         | (\<exists>b<a. f`b \<noteq> 0 \<and> (\<forall>g<a. \<forall>d<a. u(f,b,g,d) \<noteq> 0 \<longrightarrow>   
                                         u(f,b,g,d) \<approx> m))"
   unfolding lesspoll_def
 apply (blast del: equalityI)
 done
 
 (* ********************************************************************** *)
 (* Lemmas used in both cases                                              *)
 (* ********************************************************************** *)
 lemma UN_oadd: "Ord(a) \<Longrightarrow> (\<Union>b<a++a. C(b)) = (\<Union>b<a. C(b) \<union> C(a++b))"
 by (blast intro: ltI lt_oadd1 oadd_lt_mono2 dest!: lt_oadd_disj)
 
 
 (* ********************************************************************** *)
 (* Case 1: lemmas                                                        *)
 (* ********************************************************************** *)
 
 lemma vv1_subset: "vv1(f,m,b) \<subseteq> f`b"
 by (simp add: vv1_def Let_def domain_uu_subset)
 
 (* ********************************************************************** *)
 (* Case 1: Union of images is the whole "y"                              *)
 (* ********************************************************************** *)
 lemma UN_gg1_eq: 
   "\<lbrakk>Ord(a);  m \<in> nat\<rbrakk> \<Longrightarrow> (\<Union>b<a++a. gg1(f,a,m)`b) = (\<Union>b<a. f`b)"
 by (simp add: gg1_def UN_oadd lt_oadd1 oadd_le_self [THEN le_imp_not_lt] 
               lt_Ord odiff_oadd_inverse ltD vv1_subset [THEN Diff_partition]
               ww1_def)
 
 lemma domain_gg1: "domain(gg1(f,a,m)) = a++a"
 by (simp add: lam_funtype [THEN domain_of_fun] gg1_def)
 
 (* ********************************************************************** *)
 (* every value of defined function is less than or equipollent to m       *)
 (* ********************************************************************** *)
 lemma nested_LeastI:
      "\<lbrakk>P(a, b);  Ord(a);  Ord(b);   
          Least_a = (\<mu> a. \<exists>x. Ord(x) \<and> P(a, x))\<rbrakk>   
       \<Longrightarrow> P(Least_a, \<mu> b. P(Least_a, b))"
 apply (erule ssubst)
 apply (rule_tac Q = "\<lambda>z. P (z, \<mu> b. P (z, b))" in LeastI2)
 apply (fast elim!: LeastI)+
 done
 
 lemmas nested_Least_instance =
        nested_LeastI [of "\<lambda>g d. domain(uu(f,b,g,d)) \<noteq> 0 \<and> 
                                 domain(uu(f,b,g,d)) \<lesssim> m"] for f b m
 
 lemma gg1_lepoll_m: 
      "\<lbrakk>Ord(a);  m \<in> nat;   
          \<forall>b<a. f`b \<noteq>0 \<longrightarrow>                                        
              (\<exists>g<a. \<exists>d<a. domain(uu(f,b,g,d)) \<noteq> 0  \<and>                
                           domain(uu(f,b,g,d)) \<lesssim> m);             
          \<forall>b<a. f`b \<lesssim> succ(m);  b<a++a\<rbrakk> 
       \<Longrightarrow> gg1(f,a,m)`b \<lesssim> m"
 apply (simp add: gg1_def empty_lepollI)
 apply (safe dest!: lt_oadd_odiff_disj)
 (*Case b<a   \<in> show vv1(f,m,b) \<lesssim> m *)
  apply (simp add: vv1_def Let_def empty_lepollI)
  apply (fast intro: nested_Least_instance [THEN conjunct2]
              elim!: lt_Ord)
 (*Case a\<le>b \<in> show ww1(f,m,b--a) \<lesssim> m *)
 apply (simp add: ww1_def empty_lepollI)
 apply (case_tac "f` (b--a) = 0", simp add: empty_lepollI)
 apply (rule Diff_lepoll, blast)
 apply (rule vv1_subset)
 apply (drule ospec [THEN mp], assumption+)
 apply (elim oexE conjE)
 apply (simp add: vv1_def Let_def lt_Ord nested_Least_instance [THEN conjunct1])
 done
 
 (* ********************************************************************** *)
 (* Case 2: lemmas                                                        *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
 (* Case 2: vv2_subset                                                    *)
 (* ********************************************************************** *)
 
 lemma ex_d_uu_not_empty:
      "\<lbrakk>b<a;  g<a;  f`b\<noteq>0;  f`g\<noteq>0;         
          y*y \<subseteq> y;  (\<Union>b<a. f`b)=y\<rbrakk> 
       \<Longrightarrow> \<exists>d<a. uu(f,b,g,d) \<noteq> 0"
 by (unfold uu_def, blast) 
 
 lemma uu_not_empty:
      "\<lbrakk>b<a; g<a; f`b\<noteq>0; f`g\<noteq>0;  y*y \<subseteq> y; (\<Union>b<a. f`b)=y\<rbrakk>   
       \<Longrightarrow> uu(f,b,g,\<mu> d. (uu(f,b,g,d) \<noteq> 0)) \<noteq> 0"
 apply (drule ex_d_uu_not_empty, assumption+)
 apply (fast elim!: LeastI lt_Ord)
 done
 
 lemma not_empty_rel_imp_domain: "\<lbrakk>r \<subseteq> A*B; r\<noteq>0\<rbrakk> \<Longrightarrow> domain(r)\<noteq>0"
 by blast
 
 lemma Least_uu_not_empty_lt_a:
      "\<lbrakk>b<a; g<a; f`b\<noteq>0; f`g\<noteq>0; y*y \<subseteq> y; (\<Union>b<a. f`b)=y\<rbrakk>   
       \<Longrightarrow> (\<mu> d. uu(f,b,g,d) \<noteq> 0) < a"
 apply (erule ex_d_uu_not_empty [THEN oexE], assumption+)
 apply (blast intro: Least_le [THEN lt_trans1] lt_Ord)
 done
 
 lemma subset_Diff_sing: "\<lbrakk>B \<subseteq> A; a\<notin>B\<rbrakk> \<Longrightarrow> B \<subseteq> A-{a}"
 by blast
 
 (*Could this be proved more directly?*)
 lemma supset_lepoll_imp_eq:
      "\<lbrakk>A \<lesssim> m; m \<lesssim> B; B \<subseteq> A; m \<in> nat\<rbrakk> \<Longrightarrow> A=B"
 apply (erule natE)
 apply (fast dest!: lepoll_0_is_0 intro!: equalityI)
 apply (safe intro!: equalityI)
 apply (rule ccontr)
 apply (rule succ_lepoll_natE)
  apply (erule lepoll_trans)  
  apply (rule lepoll_trans)  
   apply (erule subset_Diff_sing [THEN subset_imp_lepoll], assumption)
  apply (rule Diff_sing_lepoll, assumption+) 
 done
 
 lemma uu_Least_is_fun:
      "\<lbrakk>\<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 \<longrightarrow>                
           domain(uu(f, b, g, d)) \<approx> succ(m);                         
           \<forall>b<a. f`b \<lesssim> succ(m);  y*y \<subseteq> y;                        
           (\<Union>b<a. f`b)=y;  b<a;  g<a;  d<a;                             
           f`b\<noteq>0;  f`g\<noteq>0;  m \<in> nat;  s \<in> f`b\<rbrakk> 
       \<Longrightarrow> uu(f, b, g, \<mu> d. uu(f,b,g,d)\<noteq>0) \<in> f`b -> f`g"
 apply (drule_tac x2=g in ospec [THEN ospec, THEN mp])
    apply (rule_tac [3] not_empty_rel_imp_domain [OF uu_subset1 uu_not_empty])
         apply (rule_tac [2] Least_uu_not_empty_lt_a, assumption+)
 apply (rule rel_is_fun)
     apply (erule eqpoll_sym [THEN eqpoll_imp_lepoll]) 
    apply (erule uu_lepoll_m) 
    apply (rule Least_uu_not_empty_lt_a, assumption+) 
 apply (rule uu_subset1)
 apply (rule supset_lepoll_imp_eq [OF _ eqpoll_sym [THEN eqpoll_imp_lepoll]])
 apply (fast intro!: domain_uu_subset)+
 done
 
 lemma vv2_subset: 
      "\<lbrakk>\<forall>g<a. \<forall>d<a. domain(uu(f, b, g, d))\<noteq>0 \<longrightarrow>             
                        domain(uu(f, b, g, d)) \<approx> succ(m);
          \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;
          (\<Union>b<a. f`b)=y;  b<a;  g<a;  m \<in> nat;  s \<in> f`b\<rbrakk> 
       \<Longrightarrow> vv2(f,b,g,s) \<subseteq> f`g"
 apply (simp add: vv2_def)
 apply (blast intro: uu_Least_is_fun [THEN apply_type])
 done
 
 (* ********************************************************************** *)
 (* Case 2: Union of images is the whole "y"                              *)
 (* ********************************************************************** *)
 lemma UN_gg2_eq: 
      "\<lbrakk>\<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<longrightarrow>              
                domain(uu(f,b,g,d)) \<approx> succ(m);                         
          \<forall>b<a. f`b \<lesssim> succ(m); y*y \<subseteq> y;                        
          (\<Union>b<a. f`b)=y;  Ord(a);  m \<in> nat;  s \<in> f`b;  b<a\<rbrakk> 
       \<Longrightarrow> (\<Union>g<a++a. gg2(f,a,b,s) ` g) = y"
   unfolding gg2_def
 apply (drule sym) 
 apply (simp add: ltD UN_oadd  oadd_le_self [THEN le_imp_not_lt] 
                  lt_Ord odiff_oadd_inverse ww2_def 
                  vv2_subset [THEN Diff_partition])
 done
 
 lemma domain_gg2: "domain(gg2(f,a,b,s)) = a++a"
 by (simp add: lam_funtype [THEN domain_of_fun] gg2_def)
 
 
 (* ********************************************************************** *)
 (* every value of defined function is less than or equipollent to m       *)
 (* ********************************************************************** *)
 
 lemma vv2_lepoll: "\<lbrakk>m \<in> nat; m\<noteq>0\<rbrakk> \<Longrightarrow> vv2(f,b,g,s) \<lesssim> m"
   unfolding vv2_def
 apply (simp add: empty_lepollI)
 apply (fast dest!: le_imp_subset [THEN subset_imp_lepoll, THEN lepoll_0_is_0] 
        intro!: singleton_eqpoll_1 [THEN eqpoll_imp_lepoll, THEN lepoll_trans]
                not_lt_imp_le [THEN le_imp_subset, THEN subset_imp_lepoll]
                nat_into_Ord nat_1I)
 done
 
 lemma ww2_lepoll: 
     "\<lbrakk>\<forall>b<a. f`b \<lesssim> succ(m);  g<a;  m \<in> nat;  vv2(f,b,g,d) \<subseteq> f`g\<rbrakk>  
      \<Longrightarrow> ww2(f,b,g,d) \<lesssim> m"
   unfolding ww2_def
 apply (case_tac "f`g = 0")
 apply (simp add: empty_lepollI)
 apply (drule ospec, assumption)
 apply (rule Diff_lepoll, assumption+)
 apply (simp add: vv2_def not_emptyI)
 done
 
 lemma gg2_lepoll_m: 
      "\<lbrakk>\<forall>g<a. \<forall>d<a. domain(uu(f,b,g,d)) \<noteq> 0 \<longrightarrow>              
                       domain(uu(f,b,g,d)) \<approx> succ(m);                         
          \<forall>b<a. f`b \<lesssim> succ(m);  y*y \<subseteq> y;                     
          (\<Union>b<a. f`b)=y;  b<a;  s \<in> f`b;  m \<in> nat;  m\<noteq> 0;  g<a++a\<rbrakk> 
       \<Longrightarrow> gg2(f,a,b,s) ` g \<lesssim> m"
 apply (simp add: gg2_def empty_lepollI)
 apply (safe elim!: lt_Ord2 dest!: lt_oadd_odiff_disj)
  apply (simp add: vv2_lepoll)
 apply (simp add: ww2_lepoll vv2_subset)
 done
 
 (* ********************************************************************** *)
 (* lemma ii                                                               *)
 (* ********************************************************************** *)
 lemma lemma_ii: "\<lbrakk>succ(m) \<in> NN(y); y*y \<subseteq> y; m \<in> nat; m\<noteq>0\<rbrakk> \<Longrightarrow> m \<in> NN(y)"
   unfolding NN_def
 apply (elim CollectE exE conjE) 
 apply (rule quant_domain_uu_lepoll_m [THEN cases, THEN disjE], assumption)
 (* case 1 *)
 apply (simp add: lesspoll_succ_iff)
 apply (rule_tac x = "a++a" in exI)
 apply (fast intro!: Ord_oadd domain_gg1 UN_gg1_eq gg1_lepoll_m)
 (* case 2 *)
 apply (elim oexE conjE)
 apply (rule_tac A = "f`B" for B in not_emptyE, assumption)
 apply (rule CollectI)
 apply (erule succ_natD)
 apply (rule_tac x = "a++a" in exI)
 apply (rule_tac x = "gg2 (f,a,b,x) " in exI)
 apply (simp add: Ord_oadd domain_gg2 UN_gg2_eq gg2_lepoll_m)
 done
 
 
 (* ********************************************************************** *)
 (* lemma iv - p. 4:                                                       *)
 (* For every set x there is a set y such that   x \<union> (y * y) \<subseteq> y         *)
 (* ********************************************************************** *)
 
 
 (* The leading \<forall>-quantifier looks odd but makes the proofs shorter 
    (used only in the following two lemmas)                          *)
 
 lemma z_n_subset_z_succ_n:
      "\<forall>n \<in> nat. rec(n, x, \<lambda>k r. r \<union> r*r) \<subseteq> rec(succ(n), x, \<lambda>k r. r \<union> r*r)"
 by (fast intro: rec_succ [THEN ssubst])
 
 lemma le_subsets:
      "\<lbrakk>\<forall>n \<in> nat. f(n)<=f(succ(n)); n\<le>m; n \<in> nat; m \<in> nat\<rbrakk>   
       \<Longrightarrow> f(n)<=f(m)"
 apply (erule_tac P = "n\<le>m" in rev_mp)
 apply (rule_tac P = "\<lambda>z. n\<le>z \<longrightarrow> f (n) \<subseteq> f (z) " in nat_induct) 
 apply (auto simp add: le_iff) 
 done
 
 lemma le_imp_rec_subset:
      "\<lbrakk>n\<le>m; m \<in> nat\<rbrakk> 
       \<Longrightarrow> rec(n, x, \<lambda>k r. r \<union> r*r) \<subseteq> rec(m, x, \<lambda>k r. r \<union> r*r)"
 apply (rule z_n_subset_z_succ_n [THEN le_subsets])
 apply (blast intro: lt_nat_in_nat)+
 done
 
 lemma lemma_iv: "\<exists>y. x \<union> y*y \<subseteq> y"
 apply (rule_tac x = "\<Union>n \<in> nat. rec (n, x, \<lambda>k r. r \<union> r*r) " in exI)
 apply safe
 apply (rule nat_0I [THEN UN_I], simp)
 apply (rule_tac a = "succ (n \<union> na) " in UN_I)
 apply (erule Un_nat_type [THEN nat_succI], assumption)
 apply (auto intro: le_imp_rec_subset [THEN subsetD] 
             intro!: Un_upper1_le Un_upper2_le Un_nat_type 
             elim!: nat_into_Ord)
 done
 
 (* ********************************************************************** *)
-(* Rubin \<and> Rubin wrote,                                                   *)
+(* Rubin & Rubin wrote,                                                   *)
 (* "It follows from (ii) and mathematical induction that if y*y \<subseteq> y then *)
 (* y can be well-ordered"                                                 *)
 
 (* In fact we have to prove                                               *)
 (*      * WO6 \<Longrightarrow> NN(y) \<noteq> 0                                              *)
 (*      * reverse induction which lets us infer that 1 \<in> NN(y)            *)
 (*      * 1 \<in> NN(y) \<Longrightarrow> y can be well-ordered                             *)
 (* ********************************************************************** *)
 
 (* ********************************************************************** *)
 (*      WO6 \<Longrightarrow> NN(y) \<noteq> 0                                                *)
 (* ********************************************************************** *)
 
 lemma WO6_imp_NN_not_empty: "WO6 \<Longrightarrow> NN(y) \<noteq> 0"
 by (unfold WO6_def NN_def, clarify, blast)
 
 (* ********************************************************************** *)
 (*      1 \<in> NN(y) \<Longrightarrow> y can be well-ordered                               *)
 (* ********************************************************************** *)
 
 lemma lemma1:
      "\<lbrakk>(\<Union>b<a. f`b)=y; x \<in> y; \<forall>b<a. f`b \<lesssim> 1; Ord(a)\<rbrakk> \<Longrightarrow> \<exists>c<a. f`c = {x}"
 by (fast elim!: lepoll_1_is_sing)
 
 lemma lemma2:
      "\<lbrakk>(\<Union>b<a. f`b)=y; x \<in> y; \<forall>b<a. f`b \<lesssim> 1; Ord(a)\<rbrakk>   
       \<Longrightarrow> f` (\<mu> i. f`i = {x}) = {x}"
 apply (drule lemma1, assumption+)
 apply (fast elim!: lt_Ord intro: LeastI)
 done
 
 lemma NN_imp_ex_inj: "1 \<in> NN(y) \<Longrightarrow> \<exists>a f. Ord(a) \<and> f \<in> inj(y, a)"
   unfolding NN_def
 apply (elim CollectE exE conjE)
 apply (rule_tac x = a in exI)
 apply (rule_tac x = "\<lambda>x \<in> y. \<mu> i. f`i = {x}" in exI)
 apply (rule conjI, assumption)
 apply (rule_tac d = "\<lambda>i. THE x. x \<in> f`i" in lam_injective)
 apply (drule lemma1, assumption+)
 apply (fast elim!: Least_le [THEN lt_trans1, THEN ltD] lt_Ord)
 apply (rule lemma2 [THEN ssubst], assumption+, blast)
 done
 
 lemma y_well_ord: "\<lbrakk>y*y \<subseteq> y; 1 \<in> NN(y)\<rbrakk> \<Longrightarrow> \<exists>r. well_ord(y, r)"
 apply (drule NN_imp_ex_inj)
 apply (fast elim!: well_ord_rvimage [OF _ well_ord_Memrel])
 done
 
 (* ********************************************************************** *)
 (*      reverse induction which lets us infer that 1 \<in> NN(y)              *)
 (* ********************************************************************** *)
 
 lemma rev_induct_lemma [rule_format]: 
      "\<lbrakk>n \<in> nat; \<And>m. \<lbrakk>m \<in> nat; m\<noteq>0; P(succ(m))\<rbrakk> \<Longrightarrow> P(m)\<rbrakk>   
       \<Longrightarrow> n\<noteq>0 \<longrightarrow> P(n) \<longrightarrow> P(1)"
 by (erule nat_induct, blast+)
 
 lemma rev_induct:
      "\<lbrakk>n \<in> nat;  P(n);  n\<noteq>0;   
          \<And>m. \<lbrakk>m \<in> nat; m\<noteq>0; P(succ(m))\<rbrakk> \<Longrightarrow> P(m)\<rbrakk>   
       \<Longrightarrow> P(1)"
 by (rule rev_induct_lemma, blast+)
 
 lemma NN_into_nat: "n \<in> NN(y) \<Longrightarrow> n \<in> nat"
 by (simp add: NN_def)
 
 lemma lemma3: "\<lbrakk>n \<in> NN(y); y*y \<subseteq> y; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 \<in> NN(y)"
 apply (rule rev_induct [OF NN_into_nat], assumption+)
 apply (rule lemma_ii, assumption+)
 done
 
 (* ********************************************************************** *)
 (* Main theorem "WO6 \<Longrightarrow> WO1"                                             *)
 (* ********************************************************************** *)
 
 (* another helpful lemma *)
 lemma NN_y_0: "0 \<in> NN(y) \<Longrightarrow> y=0"
   unfolding NN_def 
 apply (fast intro!: equalityI dest!: lepoll_0_is_0 elim: subst)
 done
 
 lemma WO6_imp_WO1: "WO6 \<Longrightarrow> WO1"
   unfolding WO1_def
 apply (rule allI)
 apply (case_tac "A=0")
 apply (fast intro!: well_ord_Memrel nat_0I [THEN nat_into_Ord])
 apply (rule_tac x = A in lemma_iv [elim_format])
 apply (erule exE)
 apply (drule WO6_imp_NN_not_empty)
 apply (erule Un_subset_iff [THEN iffD1, THEN conjE])
 apply (erule_tac A = "NN (y) " in not_emptyE)
 apply (frule y_well_ord)
  apply (fast intro!: lemma3 dest!: NN_y_0 elim!: not_emptyE)
 apply (fast elim: well_ord_subset)
 done
 
 end
diff --git a/src/ZF/Induct/PropLog.thy b/src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy
+++ b/src/ZF/Induct/PropLog.thy
@@ -1,340 +1,340 @@
 (*  Title:      ZF/Induct/PropLog.thy
-    Author:     Tobias Nipkow \<and> Lawrence C Paulson
+    Author:     Tobias Nipkow & Lawrence C Paulson
     Copyright   1993  University of Cambridge
 *)
 
 section \<open>Meta-theory of propositional logic\<close>
 
 theory PropLog imports ZF begin
 
 text \<open>
   Datatype definition of propositional logic formulae and inductive
   definition of the propositional tautologies.
 
   Inductive definition of propositional logic.  Soundness and
   completeness w.r.t.\ truth-tables.
 
   Prove: If \<open>H |= p\<close> then \<open>G |= p\<close> where \<open>G \<in>
   Fin(H)\<close>
 \<close>
 
 
 subsection \<open>The datatype of propositions\<close>
 
 consts
   propn :: i
 
 datatype propn =
     Fls
   | Var ("n \<in> nat")    (\<open>#_\<close> [100] 100)
   | Imp ("p \<in> propn", "q \<in> propn")    (infixr \<open>\<Rightarrow>\<close> 90)
 
 
 subsection \<open>The proof system\<close>
 
 consts thms     :: "i \<Rightarrow> i"
 
 abbreviation
   thms_syntax :: "[i,i] \<Rightarrow> o"    (infixl \<open>|-\<close> 50)
   where "H |- p \<equiv> p \<in> thms(H)"
 
 inductive
   domains "thms(H)" \<subseteq> "propn"
   intros
     H:  "\<lbrakk>p \<in> H;  p \<in> propn\<rbrakk> \<Longrightarrow> H |- p"
     K:  "\<lbrakk>p \<in> propn;  q \<in> propn\<rbrakk> \<Longrightarrow> H |- p\<Rightarrow>q\<Rightarrow>p"
     S:  "\<lbrakk>p \<in> propn;  q \<in> propn;  r \<in> propn\<rbrakk>
          \<Longrightarrow> H |- (p\<Rightarrow>q\<Rightarrow>r) \<Rightarrow> (p\<Rightarrow>q) \<Rightarrow> p\<Rightarrow>r"
     DN: "p \<in> propn \<Longrightarrow> H |- ((p\<Rightarrow>Fls) \<Rightarrow> Fls) \<Rightarrow> p"
     MP: "\<lbrakk>H |- p\<Rightarrow>q;  H |- p;  p \<in> propn;  q \<in> propn\<rbrakk> \<Longrightarrow> H |- q"
   type_intros "propn.intros"
 
 declare propn.intros [simp]
 
 
 subsection \<open>The semantics\<close>
 
 subsubsection \<open>Semantics of propositional logic.\<close>
 
 consts
   is_true_fun :: "[i,i] \<Rightarrow> i"
 primrec
   "is_true_fun(Fls, t) = 0"
   "is_true_fun(Var(v), t) = (if v \<in> t then 1 else 0)"
   "is_true_fun(p\<Rightarrow>q, t) = (if is_true_fun(p,t) = 1 then is_true_fun(q,t) else 1)"
 
 definition
   is_true :: "[i,i] \<Rightarrow> o"  where
   "is_true(p,t) \<equiv> is_true_fun(p,t) = 1"
   \<comment> \<open>this definition is required since predicates can't be recursive\<close>
 
 lemma is_true_Fls [simp]: "is_true(Fls,t) \<longleftrightarrow> False"
   by (simp add: is_true_def)
 
 lemma is_true_Var [simp]: "is_true(#v,t) \<longleftrightarrow> v \<in> t"
   by (simp add: is_true_def)
 
 lemma is_true_Imp [simp]: "is_true(p\<Rightarrow>q,t) \<longleftrightarrow> (is_true(p,t)\<longrightarrow>is_true(q,t))"
   by (simp add: is_true_def)
 
 
 subsubsection \<open>Logical consequence\<close>
 
 text \<open>
   For every valuation, if all elements of \<open>H\<close> are true then so
   is \<open>p\<close>.
 \<close>
 
 definition
   logcon :: "[i,i] \<Rightarrow> o"    (infixl \<open>|=\<close> 50)  where
   "H |= p \<equiv> \<forall>t. (\<forall>q \<in> H. is_true(q,t)) \<longrightarrow> is_true(p,t)"
 
 
 text \<open>
   A finite set of hypotheses from \<open>t\<close> and the \<open>Var\<close>s in
   \<open>p\<close>.
 \<close>
 
 consts
   hyps :: "[i,i] \<Rightarrow> i"
 primrec
   "hyps(Fls, t) = 0"
   "hyps(Var(v), t) = (if v \<in> t then {#v} else {#v\<Rightarrow>Fls})"
   "hyps(p\<Rightarrow>q, t) = hyps(p,t) \<union> hyps(q,t)"
 
 
 
 subsection \<open>Proof theory of propositional logic\<close>
 
 lemma thms_mono: "G \<subseteq> H \<Longrightarrow> thms(G) \<subseteq> thms(H)"
     unfolding thms.defs
   apply (rule lfp_mono)
     apply (rule thms.bnd_mono)+
   apply (assumption | rule univ_mono basic_monos)+
   done
 
 lemmas thms_in_pl = thms.dom_subset [THEN subsetD]
 
 inductive_cases ImpE: "p\<Rightarrow>q \<in> propn"
 
 lemma thms_MP: "\<lbrakk>H |- p\<Rightarrow>q;  H |- p\<rbrakk> \<Longrightarrow> H |- q"
   \<comment> \<open>Stronger Modus Ponens rule: no typechecking!\<close>
   apply (rule thms.MP)
      apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
   done
 
 lemma thms_I: "p \<in> propn \<Longrightarrow> H |- p\<Rightarrow>p"
   \<comment> \<open>Rule is called \<open>I\<close> for Identity Combinator, not for Introduction.\<close>
   apply (rule thms.S [THEN thms_MP, THEN thms_MP])
       apply (rule_tac [5] thms.K)
        apply (rule_tac [4] thms.K)
          apply simp_all
   done
 
 
 subsubsection \<open>Weakening, left and right\<close>
 
 lemma weaken_left: "\<lbrakk>G \<subseteq> H;  G|-p\<rbrakk> \<Longrightarrow> H|-p"
   \<comment> \<open>Order of premises is convenient with \<open>THEN\<close>\<close>
   by (erule thms_mono [THEN subsetD])
 
 lemma weaken_left_cons: "H |- p \<Longrightarrow> cons(a,H) |- p"
   by (erule subset_consI [THEN weaken_left])
 
 lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
 lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]
 
 lemma weaken_right: "\<lbrakk>H |- q;  p \<in> propn\<rbrakk> \<Longrightarrow> H |- p\<Rightarrow>q"
   by (simp_all add: thms.K [THEN thms_MP] thms_in_pl)
 
 
 subsubsection \<open>The deduction theorem\<close>
 
 theorem deduction: "\<lbrakk>cons(p,H) |- q;  p \<in> propn\<rbrakk> \<Longrightarrow>  H |- p\<Rightarrow>q"
   apply (erule thms.induct)
       apply (blast intro: thms_I thms.H [THEN weaken_right])
      apply (blast intro: thms.K [THEN weaken_right])
     apply (blast intro: thms.S [THEN weaken_right])
    apply (blast intro: thms.DN [THEN weaken_right])
   apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
   done
 
 
 subsubsection \<open>The cut rule\<close>
 
 lemma cut: "\<lbrakk>H|-p;  cons(p,H) |- q\<rbrakk> \<Longrightarrow>  H |- q"
   apply (rule deduction [THEN thms_MP])
     apply (simp_all add: thms_in_pl)
   done
 
 lemma thms_FlsE: "\<lbrakk>H |- Fls; p \<in> propn\<rbrakk> \<Longrightarrow> H |- p"
   apply (rule thms.DN [THEN thms_MP])
    apply (rule_tac [2] weaken_right)
     apply (simp_all add: propn.intros)
   done
 
 lemma thms_notE: "\<lbrakk>H |- p\<Rightarrow>Fls;  H |- p;  q \<in> propn\<rbrakk> \<Longrightarrow> H |- q"
   by (erule thms_MP [THEN thms_FlsE])
 
 
 subsubsection \<open>Soundness of the rules wrt truth-table semantics\<close>
 
 theorem soundness: "H |- p \<Longrightarrow> H |= p"
     unfolding logcon_def
   apply (induct set: thms)
       apply auto
   done
 
 
 subsection \<open>Completeness\<close>
 
 subsubsection \<open>Towards the completeness proof\<close>
 
 lemma Fls_Imp: "\<lbrakk>H |- p\<Rightarrow>Fls; q \<in> propn\<rbrakk> \<Longrightarrow> H |- p\<Rightarrow>q"
   apply (frule thms_in_pl)
   apply (rule deduction)
    apply (rule weaken_left_cons [THEN thms_notE])
      apply (blast intro: thms.H elim: ImpE)+
   done
 
 lemma Imp_Fls: "\<lbrakk>H |- p;  H |- q\<Rightarrow>Fls\<rbrakk> \<Longrightarrow> H |- (p\<Rightarrow>q)\<Rightarrow>Fls"
   apply (frule thms_in_pl)
   apply (frule thms_in_pl [of concl: "q\<Rightarrow>Fls"])
   apply (rule deduction)
    apply (erule weaken_left_cons [THEN thms_MP])
    apply (rule consI1 [THEN thms.H, THEN thms_MP])
     apply (blast intro: weaken_left_cons elim: ImpE)+
   done
 
 lemma hyps_thms_if:
     "p \<in> propn \<Longrightarrow> hyps(p,t) |- (if is_true(p,t) then p else p\<Rightarrow>Fls)"
   \<comment> \<open>Typical example of strengthening the induction statement.\<close>
   apply simp
   apply (induct_tac p)
     apply (simp_all add: thms_I thms.H)
   apply (safe elim!: Fls_Imp [THEN weaken_left_Un1] Fls_Imp [THEN weaken_left_Un2])
   apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
   done
 
 lemma logcon_thms_p: "\<lbrakk>p \<in> propn;  0 |= p\<rbrakk> \<Longrightarrow> hyps(p,t) |- p"
   \<comment> \<open>Key lemma for completeness; yields a set of assumptions satisfying \<open>p\<close>\<close>
   apply (drule hyps_thms_if)
   apply (simp add: logcon_def)
   done
 
 text \<open>
   For proving certain theorems in our new propositional logic.
 \<close>
 
 lemmas propn_SIs = propn.intros deduction
   and propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]
 
 text \<open>
   The excluded middle in the form of an elimination rule.
 \<close>
 
 lemma thms_excluded_middle:
     "\<lbrakk>p \<in> propn;  q \<in> propn\<rbrakk> \<Longrightarrow> H |- (p\<Rightarrow>q) \<Rightarrow> ((p\<Rightarrow>Fls)\<Rightarrow>q) \<Rightarrow> q"
   apply (rule deduction [THEN deduction])
     apply (rule thms.DN [THEN thms_MP])
      apply (best intro!: propn_SIs intro: propn_Is)+
   done
 
 lemma thms_excluded_middle_rule:
   "\<lbrakk>cons(p,H) |- q;  cons(p\<Rightarrow>Fls,H) |- q;  p \<in> propn\<rbrakk> \<Longrightarrow> H |- q"
   \<comment> \<open>Hard to prove directly because it requires cuts\<close>
   apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
      apply (blast intro!: propn_SIs intro: propn_Is)+
   done
 
 
 subsubsection \<open>Completeness -- lemmas for reducing the set of assumptions\<close>
 
 text \<open>
   For the case \<^prop>\<open>hyps(p,t)-cons(#v,Y) |- p\<close> we also have \<^prop>\<open>hyps(p,t)-{#v} \<subseteq> hyps(p, t-{v})\<close>.
 \<close>
 
 lemma hyps_Diff:
     "p \<in> propn \<Longrightarrow> hyps(p, t-{v}) \<subseteq> cons(#v\<Rightarrow>Fls, hyps(p,t)-{#v})"
   by (induct set: propn) auto
 
 text \<open>
   For the case \<^prop>\<open>hyps(p,t)-cons(#v \<Rightarrow> Fls,Y) |- p\<close> we also have
   \<^prop>\<open>hyps(p,t)-{#v\<Rightarrow>Fls} \<subseteq> hyps(p, cons(v,t))\<close>.
 \<close>
 
 lemma hyps_cons:
     "p \<in> propn \<Longrightarrow> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v\<Rightarrow>Fls})"
   by (induct set: propn) auto
 
 text \<open>Two lemmas for use with \<open>weaken_left\<close>\<close>
 
 lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
   by blast
 
 lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))"
   by blast
 
 text \<open>
   The set \<^term>\<open>hyps(p,t)\<close> is finite, and elements have the form
   \<^term>\<open>#v\<close> or \<^term>\<open>#v\<Rightarrow>Fls\<close>; could probably prove the stronger
   \<^prop>\<open>hyps(p,t) \<in> Fin(hyps(p,0) \<union> hyps(p,nat))\<close>.
 \<close>
 
 lemma hyps_finite: "p \<in> propn \<Longrightarrow> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v\<Rightarrow>Fls})"
   by (induct set: propn) auto
 
 lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
 
 text \<open>
   Induction on the finite set of assumptions \<^term>\<open>hyps(p,t0)\<close>.  We
   may repeatedly subtract assumptions until none are left!
 \<close>
 
 lemma completeness_0_lemma [rule_format]:
     "\<lbrakk>p \<in> propn;  0 |= p\<rbrakk> \<Longrightarrow> \<forall>t. hyps(p,t) - hyps(p,t0) |- p"
   apply (frule hyps_finite)
   apply (erule Fin_induct)
    apply (simp add: logcon_thms_p Diff_0)
   txt \<open>inductive step\<close>
   apply safe
    txt \<open>Case \<^prop>\<open>hyps(p,t)-cons(#v,Y) |- p\<close>\<close>
    apply (rule thms_excluded_middle_rule)
      apply (erule_tac [3] propn.intros)
     apply (blast intro: cons_Diff_same [THEN weaken_left])
    apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
      hyps_Diff [THEN Diff_weaken_left])
   txt \<open>Case \<^prop>\<open>hyps(p,t)-cons(#v \<Rightarrow> Fls,Y) |- p\<close>\<close>
   apply (rule thms_excluded_middle_rule)
     apply (erule_tac [3] propn.intros)
    apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
      hyps_cons [THEN Diff_weaken_left])
   apply (blast intro: cons_Diff_same [THEN weaken_left])
   done
 
 
 subsubsection \<open>Completeness theorem\<close>
 
 lemma completeness_0: "\<lbrakk>p \<in> propn;  0 |= p\<rbrakk> \<Longrightarrow> 0 |- p"
   \<comment> \<open>The base case for completeness\<close>
   apply (rule Diff_cancel [THEN subst])
   apply (blast intro: completeness_0_lemma)
   done
 
 lemma logcon_Imp: "\<lbrakk>cons(p,H) |= q\<rbrakk> \<Longrightarrow> H |= p\<Rightarrow>q"
   \<comment> \<open>A semantic analogue of the Deduction Theorem\<close>
   by (simp add: logcon_def)
 
 lemma completeness:
      "H \<in> Fin(propn) \<Longrightarrow> p \<in> propn \<Longrightarrow> H |= p \<Longrightarrow> H |- p"
   apply (induct arbitrary: p set: Fin)
    apply (safe intro!: completeness_0)
   apply (rule weaken_left_cons [THEN thms_MP])
    apply (blast intro!: logcon_Imp propn.intros)
   apply (blast intro: propn_Is)
   done
 
 theorem thms_iff: "H \<in> Fin(propn) \<Longrightarrow> H |- p \<longleftrightarrow> H |= p \<and> p \<in> propn"
   by (blast intro: soundness completeness thms_in_pl)
 
 end
diff --git a/src/ZF/ex/Commutation.thy b/src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy
+++ b/src/ZF/ex/Commutation.thy
@@ -1,142 +1,142 @@
 (*  Title:      ZF/ex/Commutation.thy
-    Author:     Tobias Nipkow \<and> Sidi Ould Ehmety
+    Author:     Tobias Nipkow & Sidi Ould Ehmety
     Copyright   1995  TU Muenchen
 
 Commutation theory for proving the Church Rosser theorem.
 *)
 
 theory Commutation imports ZF begin
 
 definition
   square  :: "[i, i, i, i] \<Rightarrow> o" where
   "square(r,s,t,u) \<equiv>
     (\<forall>a b. \<langle>a,b\<rangle> \<in> r \<longrightarrow> (\<forall>c. \<langle>a, c\<rangle> \<in> s \<longrightarrow> (\<exists>x. \<langle>b,x\<rangle> \<in> t \<and> \<langle>c,x\<rangle> \<in> u)))"
 
 definition
   commute :: "[i, i] \<Rightarrow> o" where
   "commute(r,s) \<equiv> square(r,s,s,r)"
 
 definition
   diamond :: "i\<Rightarrow>o" where
   "diamond(r)   \<equiv> commute(r, r)"
 
 definition
   strip :: "i\<Rightarrow>o" where
   "strip(r) \<equiv> commute(r^*, r)"
 
 definition
   Church_Rosser :: "i \<Rightarrow> o" where
   "Church_Rosser(r) \<equiv> (\<forall>x y. \<langle>x,y\<rangle> \<in>  (r \<union> converse(r))^* \<longrightarrow>
                         (\<exists>z. \<langle>x,z\<rangle> \<in> r^* \<and> \<langle>y,z\<rangle> \<in> r^*))"
 
 definition
   confluent :: "i\<Rightarrow>o" where
   "confluent(r) \<equiv> diamond(r^*)"
 
 
 lemma square_sym: "square(r,s,t,u) \<Longrightarrow> square(s,r,u,t)"
   unfolding square_def by blast
 
 lemma square_subset: "\<lbrakk>square(r,s,t,u); t \<subseteq> t'\<rbrakk> \<Longrightarrow> square(r,s,t',u)"
   unfolding square_def by blast
 
 
 lemma square_rtrancl:
   "square(r,s,s,t) \<Longrightarrow> field(s)<=field(t) \<Longrightarrow> square(r^*,s,s,t^*)"
 apply (unfold square_def, clarify)
 apply (erule rtrancl_induct)
 apply (blast intro: rtrancl_refl)
 apply (blast intro: rtrancl_into_rtrancl)
 done
 
 (* A special case of square_rtrancl_on *)
 lemma diamond_strip:
   "diamond(r) \<Longrightarrow> strip(r)"
   unfolding diamond_def commute_def strip_def
 apply (rule square_rtrancl, simp_all)
 done
 
 (*** commute ***)
 
 lemma commute_sym: "commute(r,s) \<Longrightarrow> commute(s,r)"
   unfolding commute_def by (blast intro: square_sym)
 
 lemma commute_rtrancl:
   "commute(r,s) \<Longrightarrow> field(r)=field(s) \<Longrightarrow> commute(r^*,s^*)"
   unfolding commute_def
 apply (rule square_rtrancl)
 apply (rule square_sym [THEN square_rtrancl, THEN square_sym])
 apply (simp_all add: rtrancl_field)
 done
 
 
 lemma confluentD: "confluent(r) \<Longrightarrow> diamond(r^*)"
 by (simp add: confluent_def)
 
 lemma strip_confluent: "strip(r) \<Longrightarrow> confluent(r)"
   unfolding strip_def confluent_def diamond_def
 apply (drule commute_rtrancl)
 apply (simp_all add: rtrancl_field)
 done
 
 lemma commute_Un: "\<lbrakk>commute(r,t); commute(s,t)\<rbrakk> \<Longrightarrow> commute(r \<union> s, t)"
   unfolding commute_def square_def by blast
 
 lemma diamond_Un:
      "\<lbrakk>diamond(r); diamond(s); commute(r, s)\<rbrakk> \<Longrightarrow> diamond(r \<union> s)"
   unfolding diamond_def by (blast intro: commute_Un commute_sym)
 
 lemma diamond_confluent:
     "diamond(r) \<Longrightarrow> confluent(r)"
   unfolding diamond_def confluent_def
 apply (erule commute_rtrancl, simp)
 done
 
 lemma confluent_Un:
  "\<lbrakk>confluent(r); confluent(s); commute(r^*, s^*);
      relation(r); relation(s)\<rbrakk> \<Longrightarrow> confluent(r \<union> s)"
   unfolding confluent_def
 apply (rule rtrancl_Un_rtrancl [THEN subst], auto)
 apply (blast dest: diamond_Un intro: diamond_confluent [THEN confluentD])
 done
 
 
 lemma diamond_to_confluence:
      "\<lbrakk>diamond(r); s \<subseteq> r; r<= s^*\<rbrakk> \<Longrightarrow> confluent(s)"
 apply (drule rtrancl_subset [symmetric], assumption)
 apply (simp_all add: confluent_def)
 apply (blast intro: diamond_confluent [THEN confluentD])
 done
 
 
 (*** Church_Rosser ***)
 
 lemma Church_Rosser1:
      "Church_Rosser(r) \<Longrightarrow> confluent(r)"
 apply (unfold confluent_def Church_Rosser_def square_def
               commute_def diamond_def, auto)
 apply (drule converseI)
 apply (simp (no_asm_use) add: rtrancl_converse [symmetric])
 apply (drule_tac x = b in spec)
 apply (drule_tac x1 = c in spec [THEN mp])
 apply (rule_tac b = a in rtrancl_trans)
 apply (blast intro: rtrancl_mono [THEN subsetD])+
 done
 
 
 lemma Church_Rosser2:
      "confluent(r) \<Longrightarrow> Church_Rosser(r)"
 apply (unfold confluent_def Church_Rosser_def square_def
               commute_def diamond_def, auto)
 apply (frule fieldI1)
 apply (simp add: rtrancl_field)
 apply (erule rtrancl_induct, auto)
 apply (blast intro: rtrancl_refl)
 apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)+
 done
 
 
 lemma Church_Rosser: "Church_Rosser(r) \<longleftrightarrow> confluent(r)"
   by (blast intro: Church_Rosser1 Church_Rosser2)
 
 end
diff --git a/src/ZF/ex/NatSum.thy b/src/ZF/ex/NatSum.thy
--- a/src/ZF/ex/NatSum.thy
+++ b/src/ZF/ex/NatSum.thy
@@ -1,69 +1,69 @@
 (*  Title:      ZF/ex/NatSum.thy
-    Author:     Tobias Nipkow \<and> Lawrence C Paulson
+    Author:     Tobias Nipkow & Lawrence C Paulson
 
 A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
 
 Note: n is a natural number but the sum is an integer,
                             and f maps integers to integers
 
 Summing natural numbers, squares, cubes, etc.
 
 Originally demonstrated permutative rewriting, but add_ac is no longer needed
   thanks to new simprocs.
 
 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
   http://www.research.att.com/\<not>njas/sequences/
 *)
 
 
 theory NatSum imports ZF begin
 
 consts sum :: "[i\<Rightarrow>i, i] \<Rightarrow> i"
 primrec 
   "sum (f,0) = #0"
   "sum (f, succ(n)) = f($#n) $+ sum(f,n)"
 
 declare zadd_zmult_distrib [simp]  zadd_zmult_distrib2 [simp]
 declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp]
 
 (*The sum of the first n odd numbers equals n squared.*)
 lemma sum_of_odds: "n \<in> nat \<Longrightarrow> sum (\<lambda>i. i $+ i $+ #1, n) = $#n $* $#n"
 by (induct_tac "n", auto)
 
 (*The sum of the first n odd squares*)
 lemma sum_of_odd_squares:
      "n \<in> nat \<Longrightarrow> #3 $* sum (\<lambda>i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) =  
       $#n $* (#4 $* $#n $* $#n $- #1)"
 by (induct_tac "n", auto)
 
 (*The sum of the first n odd cubes*)
 lemma sum_of_odd_cubes:
      "n \<in> nat  
       \<Longrightarrow> sum (\<lambda>i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) =  
           $#n $* $#n $* (#2 $* $#n $* $#n $- #1)"
 by (induct_tac "n", auto)
 
 (*The sum of the first n positive integers equals n(n+1)/2.*)
 lemma sum_of_naturals:
      "n \<in> nat \<Longrightarrow> #2 $* sum(\<lambda>i. i, succ(n)) = $#n $* $#succ(n)"
 by (induct_tac "n", auto)
 
 lemma sum_of_squares:
      "n \<in> nat \<Longrightarrow> #6 $* sum (\<lambda>i. i$*i, succ(n)) =  
                   $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)"
 by (induct_tac "n", auto)
 
 lemma sum_of_cubes:
      "n \<in> nat \<Longrightarrow> #4 $* sum (\<lambda>i. i$*i$*i, succ(n)) =  
                   $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)"
 by (induct_tac "n", auto)
 
 (** Sum of fourth powers **)
 
 lemma sum_of_fourth_powers:
      "n \<in> nat \<Longrightarrow> #30 $* sum (\<lambda>i. i$*i$*i$*i, succ(n)) =  
                     $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $*  
                     (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)"
 by (induct_tac "n", auto)
 
 end