lexical tidying
authorpaulson
Mon Jan 21 11:25:45 2002 +0100 (2002-01-21)
changeset 1282002e2ff3e4d37
parent 12819 2f61bca07de7
child 12821 ed702a3af45c
lexical tidying
src/ZF/AC/AC15_WO6.thy
src/ZF/AC/AC16_WO4.thy
src/ZF/AC/AC16_lemmas.thy
src/ZF/AC/AC18_AC19.thy
src/ZF/AC/AC_Equiv.thy
src/ZF/AC/Cardinal_aux.thy
src/ZF/AC/DC.thy
src/ZF/AC/HH.thy
src/ZF/AC/Hartog.thy
src/ZF/AC/WO1_WO7.thy
src/ZF/AC/WO2_AC16.thy
src/ZF/AC/WO6_WO1.thy
src/ZF/CardinalArith.thy
src/ZF/Main.thy
src/ZF/OrdQuant.thy
     1.1 --- a/src/ZF/AC/AC15_WO6.thy	Mon Jan 21 10:52:05 2002 +0100
     1.2 +++ b/src/ZF/AC/AC15_WO6.thy	Mon Jan 21 11:25:45 2002 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  apply (drule subset_consI [THEN subset_imp_lepoll, THEN lepoll_Finite])
     1.5  apply (rule nat_not_Finite [THEN notE] )
     1.6  apply (subgoal_tac "x ~= 0")
     1.7 -apply (blast intro: lepoll_Sigma [THEN lepoll_Finite] , blast) 
     1.8 +apply (blast intro: lepoll_Sigma [THEN lepoll_Finite], blast) 
     1.9  done
    1.10  
    1.11  lemma lemma1: "[| Union(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
    1.12 @@ -61,8 +61,7 @@
    1.13  apply (unfold sets_of_size_between_def)
    1.14  apply (rule ballI)
    1.15  apply (erule_tac x="cons(0, B*nat)" in ballE)
    1.16 - apply (blast dest: lemma1 intro!: lemma2) 
    1.17 -apply blast
    1.18 + apply (blast dest: lemma1 intro!: lemma2, blast)
    1.19  done
    1.20  
    1.21  lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i"
    1.22 @@ -180,7 +179,7 @@
    1.23  apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
    1.24  apply simp
    1.25  apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
    1.26 -            elim!: less_Least_subset_x lemma1 lemma2, assumption); 
    1.27 +            elim!: less_Least_subset_x lemma1 lemma2, assumption) 
    1.28  done
    1.29  
    1.30  
    1.31 @@ -199,7 +198,7 @@
    1.32  theorem AC10_AC13: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC13(n)"
    1.33  apply (unfold AC10_def AC13_def, safe)
    1.34  apply (erule allE) 
    1.35 -apply (erule impE [OF _ cons_times_nat_not_Finite], assumption); 
    1.36 +apply (erule impE [OF _ cons_times_nat_not_Finite], assumption) 
    1.37  apply (fast elim!: impE [OF _ cons_times_nat_not_Finite] 
    1.38              dest!: ex_fun_AC13_AC15)
    1.39  done
     2.1 --- a/src/ZF/AC/AC16_WO4.thy	Mon Jan 21 10:52:05 2002 +0100
     2.2 +++ b/src/ZF/AC/AC16_WO4.thy	Mon Jan 21 11:25:45 2002 +0100
     2.3 @@ -144,7 +144,7 @@
     2.4  apply (erule impE)
     2.5  apply (simp add: add_succ)
     2.6  apply (fast intro!: Diff_sing_eqpoll lepoll_Diff_sing) 
     2.7 -apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp); 
     2.8 +apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
     2.9  apply blast 
    2.10  done
    2.11  
    2.12 @@ -171,7 +171,7 @@
    2.13  apply (erule_tac x = "B - {xa}" in allE)
    2.14  apply (erule impE)
    2.15  apply (force intro: eqpoll_sym intro!: Diff_sing_eqpoll)
    2.16 -apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp); 
    2.17 +apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
    2.18  apply blast 
    2.19  done
    2.20  
    2.21 @@ -361,7 +361,7 @@
    2.22  (** LEVEL 8 **)
    2.23  apply (rule w_Int_eqpoll_m [THEN eqpoll_m_not_empty, THEN not_emptyE])
    2.24  apply (blast, assumption+)
    2.25 -apply (drule equalityD1 [THEN subsetD], (assumption))
    2.26 +apply (drule equalityD1 [THEN subsetD], assumption)
    2.27  apply (frule cons_cons_in, assumption+)
    2.28  apply (blast dest: ex1_two_eq intro: s_subset [THEN subsetD] in_s_imp_u_in)+
    2.29  done
    2.30 @@ -385,7 +385,7 @@
    2.31  apply (erule exE)
    2.32  apply (rule well_ord_subsets_eqpoll_n [THEN exE], assumption)
    2.33  apply (simp add: subsets_lepoll_succ)
    2.34 -apply (drule well_ord_radd, (assumption))
    2.35 +apply (drule well_ord_radd, assumption)
    2.36  apply (erule Int_empty [THEN disj_Un_eqpoll_sum,
    2.37                    THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
    2.38  apply (fast elim!: bij_is_inj [THEN well_ord_rvimage])
    2.39 @@ -410,9 +410,8 @@
    2.40  
    2.41  lemma (in AC16) unique_superset_in_MM:
    2.42       "v \<in> LL ==> \<exists>! w. w \<in> MM & v \<subseteq> w"
    2.43 -apply (unfold MM_def LL_def, safe)
    2.44 -apply fast
    2.45 -apply (rule lepoll_imp_eqpoll_subset [THEN exE], (assumption))
    2.46 +apply (unfold MM_def LL_def, safe, fast)
    2.47 +apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
    2.48  apply (rule_tac x = "x" in all_ex [THEN ballE]) 
    2.49  apply (blast intro: eqpoll_sym)+
    2.50  done
     3.1 --- a/src/ZF/AC/AC16_lemmas.thy	Mon Jan 21 10:52:05 2002 +0100
     3.2 +++ b/src/ZF/AC/AC16_lemmas.thy	Mon Jan 21 11:25:45 2002 +0100
     3.3 @@ -40,8 +40,7 @@
     3.4  apply (fast intro!: RepFunI)
     3.5  apply (rule subsetI)
     3.6  apply (erule RepFunE)
     3.7 -apply (rule CollectI)
     3.8 -apply fast
     3.9 +apply (rule CollectI, fast)
    3.10  apply (fast intro!: singleton_eqpoll_1)
    3.11  done
    3.12  
    3.13 @@ -49,10 +48,8 @@
    3.14  apply (unfold eqpoll_def bij_def)
    3.15  apply (rule_tac x = "\<lambda>x \<in> X. {x}" in exI)
    3.16  apply (rule IntI)
    3.17 -apply (unfold inj_def surj_def)
    3.18 -apply simp
    3.19 -apply (fast intro!: lam_type RepFunI intro: singleton_eq_iff [THEN iffD1])
    3.20 -apply simp
    3.21 +apply (unfold inj_def surj_def, simp)
    3.22 +apply (fast intro!: lam_type RepFunI intro: singleton_eq_iff [THEN iffD1], simp)
    3.23  apply (fast intro!: lam_type)
    3.24  done
    3.25  
    3.26 @@ -76,15 +73,15 @@
    3.27  apply (unfold lepoll_def)
    3.28  apply (rule_tac x = "\<lambda>y \<in> {y \<in> Pow(x) . y\<approx>succ (succ (n))}. 
    3.29                        <LEAST i. i \<in> y, y-{LEAST i. i \<in> y}>" in exI)
    3.30 -apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective);
    3.31 - apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in);
    3.32 -apply (simp, blast intro: InfCard_Least_in);
    3.33 +apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective)
    3.34 + apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in)
    3.35 +apply (simp, blast intro: InfCard_Least_in)
    3.36  done
    3.37  
    3.38  lemma set_of_Ord_succ_Union: "(\<forall>y \<in> z. Ord(y)) ==> z \<subseteq> succ(Union(z))"
    3.39  apply (rule subsetI)
    3.40 -apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast );
    3.41 -apply (simp, erule bexE); 
    3.42 +apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast )
    3.43 +apply (simp, erule bexE) 
    3.44  apply (rule_tac i=xa and j=x in Ord_linear_le)
    3.45  apply (blast dest: le_imp_subset elim: leE ltE)+
    3.46  done
    3.47 @@ -94,8 +91,7 @@
    3.48  
    3.49  lemma succ_Union_not_mem:
    3.50       "(!!y. y \<in> z ==> Ord(y)) ==> succ(Union(z)) \<notin> z"
    3.51 -apply (rule set_of_Ord_succ_Union [THEN subset_not_mem]);
    3.52 -apply blast
    3.53 +apply (rule set_of_Ord_succ_Union [THEN subset_not_mem], blast)
    3.54  done
    3.55  
    3.56  lemma Union_cons_eq_succ_Union:
    3.57 @@ -115,35 +111,31 @@
    3.58  apply (intro allI impI)
    3.59  apply (erule natE)
    3.60  apply (fast dest!: eqpoll_1_iff_singleton [THEN iffD1]
    3.61 -            intro!: Union_singleton)
    3.62 -apply (clarify ); 
    3.63 +            intro!: Union_singleton, clarify) 
    3.64  apply (elim not_emptyE)
    3.65  apply (erule_tac x = "z-{xb}" in allE)
    3.66  apply (erule impE)
    3.67  apply (fast elim!: Diff_sing_eqpoll
    3.68                     Diff_sing_eqpoll [THEN eqpoll_succ_imp_not_empty])
    3.69 -apply (subgoal_tac "xb \<union> \<Union>(z - {xb}) \<in> z");
    3.70 -apply (simp add: Union_eq_Un [symmetric]);
    3.71 +apply (subgoal_tac "xb \<union> \<Union>(z - {xb}) \<in> z")
    3.72 +apply (simp add: Union_eq_Un [symmetric])
    3.73  apply (frule bspec, assumption)
    3.74 -apply (drule bspec); 
    3.75 -apply (erule Diff_subset [THEN subsetD]);
    3.76 -apply (drule Un_Ord_disj, assumption)
    3.77 -apply (auto ); 
    3.78 +apply (drule bspec) 
    3.79 +apply (erule Diff_subset [THEN subsetD])
    3.80 +apply (drule Un_Ord_disj, assumption, auto) 
    3.81  done
    3.82  
    3.83  lemma Union_in: "[| \<forall>x \<in> z. Ord(x); z\<approx>n; z\<noteq>0; n \<in> nat |] ==> Union(z) \<in> z"
    3.84 -apply (blast intro: Union_in_lemma); 
    3.85 -done
    3.86 +by (blast intro: Union_in_lemma)
    3.87  
    3.88  lemma succ_Union_in_x:
    3.89       "[| InfCard(x); z \<in> Pow(x); z\<approx>n; n \<in> nat |] ==> succ(Union(z)) \<in> x"
    3.90 -apply (rule Limit_has_succ [THEN ltE]);
    3.91 +apply (rule Limit_has_succ [THEN ltE])
    3.92  prefer 3 apply assumption
    3.93  apply (erule InfCard_is_Limit)
    3.94 -apply (case_tac "z=0");
    3.95 -apply (simp, fast intro!: InfCard_is_Limit [THEN Limit_has_0]);
    3.96 -apply (rule ltI [OF PowD [THEN subsetD] InfCard_is_Card [THEN Card_is_Ord]]);
    3.97 -apply assumption; 
    3.98 +apply (case_tac "z=0")
    3.99 +apply (simp, fast intro!: InfCard_is_Limit [THEN Limit_has_0])
   3.100 +apply (rule ltI [OF PowD [THEN subsetD] InfCard_is_Card [THEN Card_is_Ord]], assumption)
   3.101  apply (blast intro: Union_in
   3.102                      InfCard_is_Card [THEN Card_is_Ord, THEN Ord_in_Ord])+
   3.103  done
   3.104 @@ -151,18 +143,18 @@
   3.105  lemma succ_lepoll_succ_succ:
   3.106       "[| InfCard(x); n \<in> nat |] 
   3.107        ==> {y \<in> Pow(x). y\<approx>succ(n)} \<lesssim> {y \<in> Pow(x). y\<approx>succ(succ(n))}"
   3.108 -apply (unfold lepoll_def);
   3.109 +apply (unfold lepoll_def)
   3.110  apply (rule_tac x = "\<lambda>z \<in> {y\<in>Pow(x). y\<approx>succ(n)}. cons(succ(Union(z)), z)" 
   3.111         in exI)
   3.112  apply (rule_tac d = "%z. z-{Union (z) }" in lam_injective)
   3.113  apply (blast intro!: succ_Union_in_x succ_Union_not_mem
   3.114               intro: cons_eqpoll_succ Ord_in_Ord
   3.115               dest!: InfCard_is_Card [THEN Card_is_Ord])
   3.116 -apply (simp only: Union_cons_eq_succ_Union); 
   3.117 -apply (rule cons_Diff_eq);
   3.118 +apply (simp only: Union_cons_eq_succ_Union) 
   3.119 +apply (rule cons_Diff_eq)
   3.120  apply (fast dest!: InfCard_is_Card [THEN Card_is_Ord]
   3.121              elim: Ord_in_Ord 
   3.122 -            intro!: succ_Union_not_mem);
   3.123 +            intro!: succ_Union_not_mem)
   3.124  done
   3.125  
   3.126  lemma subsets_eqpoll_X:
   3.127 @@ -170,9 +162,9 @@
   3.128  apply (induct_tac "n")
   3.129  apply (rule subsets_eqpoll_1_eqpoll)
   3.130  apply (rule eqpollI)
   3.131 -apply (rule subsets_lepoll_lemma1 [THEN lepoll_trans], assumption+);
   3.132 -apply (rule eqpoll_trans [THEN eqpoll_imp_lepoll]); 
   3.133 - apply (erule eqpoll_refl [THEN prod_eqpoll_cong]);
   3.134 +apply (rule subsets_lepoll_lemma1 [THEN lepoll_trans], assumption+)
   3.135 +apply (rule eqpoll_trans [THEN eqpoll_imp_lepoll]) 
   3.136 + apply (erule eqpoll_refl [THEN prod_eqpoll_cong])
   3.137  apply (erule InfCard_square_eqpoll)
   3.138  apply (fast elim: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
   3.139              intro!: succ_lepoll_succ_succ)
   3.140 @@ -185,8 +177,7 @@
   3.141  done
   3.142  
   3.143  lemma vimage_image_eq: "[| f \<in> inj(A,B); y \<subseteq> A |] ==> converse(f)``(f``y) = y"
   3.144 -apply (fast elim!: inj_is_fun [THEN apply_Pair] dest: inj_equality)
   3.145 -done
   3.146 +by (fast elim!: inj_is_fun [THEN apply_Pair] dest: inj_equality)
   3.147  
   3.148  lemma subsets_eqpoll:
   3.149       "A\<approx>B ==> {Y \<in> Pow(A). Y\<approx>n}\<approx>{Y \<in> Pow(B). Y\<approx>n}"
   3.150 @@ -222,10 +213,10 @@
   3.151  lemma WO2_infinite_subsets_eqpoll_X: "[| WO2; n \<in> nat; ~Finite(X) |]   
   3.152          ==> {Y \<in> Pow(X). Y\<approx>succ(n)}\<approx>X"
   3.153  apply (drule WO2_imp_ex_Card)
   3.154 -apply (elim allE exE conjE);
   3.155 +apply (elim allE exE conjE)
   3.156  apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
   3.157  apply (drule infinite_Card_is_InfCard, assumption)
   3.158 -apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans); 
   3.159 +apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans) 
   3.160  done
   3.161  
   3.162  lemma well_ord_imp_ex_Card: "well_ord(X,R) ==> \<exists>a. Card(a) & X\<approx>a"
   3.163 @@ -238,7 +229,7 @@
   3.164  apply (elim allE exE conjE)
   3.165  apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
   3.166  apply (drule infinite_Card_is_InfCard, assumption)
   3.167 -apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans); 
   3.168 +apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans) 
   3.169  done
   3.170  
   3.171  end
     4.1 --- a/src/ZF/AC/AC18_AC19.thy	Mon Jan 21 10:52:05 2002 +0100
     4.2 +++ b/src/ZF/AC/AC18_AC19.thy	Mon Jan 21 11:25:45 2002 +0100
     4.3 @@ -66,7 +66,7 @@
     4.4  
     4.5  lemma lemma1_1: "[|c \<in> a; x = c Un {0}; x \<notin> a |] ==> x - {0} \<in> a"
     4.6  apply clarify 
     4.7 -apply (rule subst_elem , (assumption))
     4.8 +apply (rule subst_elem, assumption)
     4.9  apply (fast elim: notE subst_elem)
    4.10  done
    4.11  
    4.12 @@ -98,10 +98,9 @@
    4.13  apply (case_tac "A=0", force)
    4.14  apply (erule_tac x = "{uu (a) . a \<in> A}" in allE)
    4.15  apply (erule impE)
    4.16 -apply (erule RepRep_conj , (assumption))
    4.17 +apply (erule RepRep_conj, assumption)
    4.18  apply (rule lemma1)
    4.19 -apply (drule lemma2 , (assumption))
    4.20 -apply auto 
    4.21 +apply (drule lemma2, assumption, auto) 
    4.22  done
    4.23  
    4.24  end
     5.1 --- a/src/ZF/AC/AC_Equiv.thy	Mon Jan 21 10:52:05 2002 +0100
     5.2 +++ b/src/ZF/AC/AC_Equiv.thy	Mon Jan 21 11:25:45 2002 +0100
     5.3 @@ -139,7 +139,7 @@
     5.4  apply (unfold rvimage_def)
     5.5  apply (rule equalityI, safe)
     5.6  apply (drule_tac P = "%a. <id (A) `xb,a>:r" in id_conv [THEN subst],
     5.7 -       (assumption))
     5.8 +       assumption)
     5.9  apply (drule_tac P = "%a. <a,ya>:r" in id_conv [THEN subst], (assumption+))
    5.10  apply (fast intro: id_conv [THEN ssubst])
    5.11  done
    5.12 @@ -179,7 +179,7 @@
    5.13  lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
    5.14  apply (unfold surj_def)
    5.15  apply (erule CollectE)
    5.16 -apply (rule image_fun [THEN ssubst], (assumption), rule subset_refl)
    5.17 +apply (rule image_fun [THEN ssubst], assumption, rule subset_refl)
    5.18  apply (blast dest: apply_type) 
    5.19  done
    5.20  
    5.21 @@ -217,7 +217,7 @@
    5.22  apply (fast intro: LeastI2 nat_into_Ord [THEN Ord_in_Ord] 
    5.23                             inj_is_fun [THEN apply_type])
    5.24  apply (erule domainE)
    5.25 -apply (frule inj_is_fun [THEN apply_type], (assumption))
    5.26 +apply (frule inj_is_fun [THEN apply_type], assumption)
    5.27  apply (rule LeastI2)
    5.28  apply (auto elim!: nat_into_Ord [THEN Ord_in_Ord])
    5.29  done
     6.1 --- a/src/ZF/AC/Cardinal_aux.thy	Mon Jan 21 10:52:05 2002 +0100
     6.2 +++ b/src/ZF/AC/Cardinal_aux.thy	Mon Jan 21 11:25:45 2002 +0100
     6.3 @@ -8,7 +8,7 @@
     6.4  theory Cardinal_aux = AC_Equiv:
     6.5  
     6.6  lemma Diff_lepoll: "[| A \<lesssim> succ(m); B \<subseteq> A; B\<noteq>0 |] ==> A-B \<lesssim> m"
     6.7 -apply (rule not_emptyE, (assumption))
     6.8 +apply (rule not_emptyE, assumption)
     6.9  apply (blast intro: lepoll_trans [OF subset_imp_lepoll Diff_sing_lepoll])
    6.10  done
    6.11  
    6.12 @@ -151,7 +151,7 @@
    6.13           ~Finite(a); Ord(a); n \<in> nat |] 
    6.14        ==> (\<Union>b \<in> a. F(b)) \<lesssim> a"
    6.15  apply (rule rev_mp) 
    6.16 -apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll);
    6.17 +apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll)
    6.18  apply auto
    6.19  done
    6.20  
    6.21 @@ -187,7 +187,7 @@
    6.22  apply (drule Un_least_lt, assumption)
    6.23  apply (drule eqpoll_imp_lepoll [THEN lepoll_trans], 
    6.24         rule le_imp_lepoll, assumption)+
    6.25 -apply (case_tac "Finite(x Un xa)");
    6.26 +apply (case_tac "Finite(x Un xa)")
    6.27  txt{*finite case*}
    6.28   apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+) 
    6.29   apply (drule subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_Finite])
     7.1 --- a/src/ZF/AC/DC.thy	Mon Jan 21 10:52:05 2002 +0100
     7.2 +++ b/src/ZF/AC/DC.thy	Mon Jan 21 11:25:45 2002 +0100
     7.3 @@ -363,8 +363,7 @@
     7.4  apply (unfold XX_def)
     7.5  apply (drule apply_type, assumption)
     7.6  apply (elim UN_E CollectE)
     7.7 -apply (drule domain_of_fun [symmetric, THEN trans], assumption)
     7.8 -apply simp
     7.9 +apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp)
    7.10  done
    7.11  
    7.12  lemma (in imp_DC0) restrict_cons_eq_restrict: 
    7.13 @@ -404,7 +403,7 @@
    7.14  (*induction step*) (** LEVEL 5 **)
    7.15  (*prevent simplification of ~\<exists> to \<forall>~ *)
    7.16  apply (simp only: separation split)
    7.17 -apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI);
    7.18 +apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI)
    7.19  apply (elim conjE disjE)
    7.20  apply (force elim!: trans subst_context
    7.21               intro!: UN_image_succ_eq_succ)
    7.22 @@ -455,8 +454,7 @@
    7.23  apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+)
    7.24  apply (unfold allRR_def)
    7.25  apply (drule ospec) 
    7.26 -apply (drule ltI [OF nat_succI Ord_nat], assumption)
    7.27 -apply simp
    7.28 +apply (drule ltI [OF nat_succI Ord_nat], assumption, simp)
    7.29  apply (elim conjE ballE)
    7.30  apply (erule restrict_eq_imp_val_eq [symmetric], force) 
    7.31  apply (simp add: image_fun OrdmemD) 
    7.32 @@ -500,7 +498,7 @@
    7.33  theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
    7.34  apply (unfold DC_def WO3_def)
    7.35  apply (rule allI)
    7.36 -apply (case_tac "A \<prec> Hartog (A)");
    7.37 +apply (case_tac "A \<prec> Hartog (A)")
    7.38  apply (fast dest!: lesspoll_imp_ex_lt_eqpoll 
    7.39              intro!: Ord_Hartog leI [THEN le_imp_subset])
    7.40  apply (erule allE impE)+
     8.1 --- a/src/ZF/AC/HH.thy	Mon Jan 21 10:52:05 2002 +0100
     8.2 +++ b/src/ZF/AC/HH.thy	Mon Jan 21 11:25:45 2002 +0100
     8.3 @@ -239,8 +239,7 @@
     8.4  apply (rule bij_Least_HH_x [THEN bij_converse_bij])
     8.5  apply (rule f_subsets_imp_UN_HH_eq_x)
     8.6  apply (intro ballI apply_type) 
     8.7 -apply (fast intro: lam_type apply_type del: DiffE)
     8.8 -apply assumption; 
     8.9 +apply (fast intro: lam_type apply_type del: DiffE, assumption) 
    8.10  apply (fast intro: Pi_weaken_type)
    8.11  done
    8.12  
     9.1 --- a/src/ZF/AC/Hartog.thy	Mon Jan 21 10:52:05 2002 +0100
     9.2 +++ b/src/ZF/AC/Hartog.thy	Mon Jan 21 11:25:45 2002 +0100
     9.3 @@ -25,7 +25,7 @@
     9.4    apply (erule inj_is_fun [THEN fun_is_rel, THEN image_subset])
     9.5   apply (rule well_ord_rvimage [OF bij_is_inj well_ord_Memrel]) 
     9.6    apply (erule restrict_bij [THEN bij_converse_bij]) 
     9.7 -apply (rule subset_refl, assumption); 
     9.8 +apply (rule subset_refl, assumption) 
     9.9  apply (rule trans) 
    9.10  apply (rule bij_ordertype_vimage) 
    9.11  apply (erule restrict_bij [THEN bij_converse_bij]) 
    9.12 @@ -36,8 +36,7 @@
    9.13  
    9.14  lemma Ord_lepoll_imp_eq_ordertype:
    9.15       "[| Ord(a); a \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & (\<exists>R. R \<subseteq> X*X & ordertype(Y,R)=a)"
    9.16 -apply (drule Ord_lepoll_imp_ex_well_ord, (assumption))
    9.17 -apply clarify
    9.18 +apply (drule Ord_lepoll_imp_ex_well_ord, assumption, clarify)
    9.19  apply (intro exI conjI)
    9.20  apply (erule_tac [3] ordertype_Int, auto) 
    9.21  done
    10.1 --- a/src/ZF/AC/WO1_WO7.thy	Mon Jan 21 10:52:05 2002 +0100
    10.2 +++ b/src/ZF/AC/WO1_WO7.thy	Mon Jan 21 11:25:45 2002 +0100
    10.3 @@ -50,7 +50,7 @@
    10.4  lemma converse_Memrel_not_wf_on: 
    10.5      "[| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"
    10.6  apply (unfold wf_on_def wf_def)
    10.7 -apply (drule nat_le_infinite_Ord [THEN le_imp_subset], (assumption))
    10.8 +apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
    10.9  apply (rule notI)
   10.10  apply (erule_tac x = "nat" in allE, blast)
   10.11  done
    11.1 --- a/src/ZF/AC/WO2_AC16.thy	Mon Jan 21 10:52:05 2002 +0100
    11.2 +++ b/src/ZF/AC/WO2_AC16.thy	Mon Jan 21 11:25:45 2002 +0100
    11.3 @@ -31,8 +31,7 @@
    11.4  (* ********************************************************************** *)
    11.5  
    11.6  lemma recfunAC16_0: "recfunAC16(f,h,0,a) = 0"
    11.7 -apply (simp add: recfunAC16_def);
    11.8 -done
    11.9 +by (simp add: recfunAC16_def)
   11.10  
   11.11  lemma recfunAC16_succ: 
   11.12       "recfunAC16(f,h,succ(i),a) =   
   11.13 @@ -41,7 +40,7 @@
   11.14              {f ` (LEAST j. h ` i \<subseteq> f ` j &   
   11.15               (\<forall>b<a. (h`b \<subseteq> f`j   
   11.16                --> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
   11.17 -apply (simp add: recfunAC16_def);
   11.18 +apply (simp add: recfunAC16_def)
   11.19  done
   11.20  
   11.21  lemma recfunAC16_Limit: "Limit(i)   
   11.22 @@ -55,12 +54,11 @@
   11.23  lemma transrec2_mono_lemma [rule_format]:
   11.24       "[| !!g r. r \<subseteq> B(g,r);  Ord(i) |]   
   11.25        ==> j<i --> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
   11.26 -apply (erule trans_induct);
   11.27 -apply (rule Ord_cases , assumption+);
   11.28 -apply fast
   11.29 +apply (erule trans_induct)
   11.30 +apply (rule Ord_cases, assumption+, fast)
   11.31  apply (simp (no_asm_simp))
   11.32 -apply (blast elim!: leE); 
   11.33 -apply (simp add: transrec2_Limit); 
   11.34 +apply (blast elim!: leE) 
   11.35 +apply (simp add: transrec2_Limit) 
   11.36  apply (blast intro: OUN_I ltI Ord_in_Ord [THEN le_refl]
   11.37               elim!: Limit_has_succ [THEN ltE])
   11.38  done
   11.39 @@ -68,9 +66,9 @@
   11.40  lemma transrec2_mono:
   11.41       "[| !!g r. r \<subseteq> B(g,r); j\<le>i |] 
   11.42        ==> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
   11.43 -apply (erule leE);
   11.44 +apply (erule leE)
   11.45  apply (rule transrec2_mono_lemma)
   11.46 -apply (auto intro: lt_Ord2 ); 
   11.47 +apply (auto intro: lt_Ord2 ) 
   11.48  done
   11.49  
   11.50  (* ********************************************************************** *)
   11.51 @@ -80,8 +78,7 @@
   11.52  lemma recfunAC16_mono: 
   11.53         "i\<le>j ==> recfunAC16(f, g, i, a) \<subseteq> recfunAC16(f, g, j, a)"
   11.54  apply (unfold recfunAC16_def)
   11.55 -apply (rule transrec2_mono)
   11.56 -apply (auto ); 
   11.57 +apply (rule transrec2_mono, auto) 
   11.58  done
   11.59  
   11.60  (* ********************************************************************** *)
   11.61 @@ -95,8 +92,7 @@
   11.62          V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]   
   11.63       ==> V = W"
   11.64  apply (erule asm_rl allE impE)+
   11.65 -apply (drule subsetD, assumption)
   11.66 -apply blast 
   11.67 +apply (drule subsetD, assumption, blast) 
   11.68  done
   11.69  
   11.70  
   11.71 @@ -118,8 +114,7 @@
   11.72        ==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) -->   
   11.73                         (\<exists>! Y. Y \<in> F(y) & h(z) \<subseteq> Y)"
   11.74  apply (intro oallI impI)
   11.75 -apply (drule ospec, assumption)
   11.76 -apply clarify
   11.77 +apply (drule ospec, assumption, clarify)
   11.78  apply (blast elim!: oallE ) 
   11.79  done
   11.80  
   11.81 @@ -134,8 +129,7 @@
   11.82  apply (rule conjI)
   11.83  apply (rule subsetI)
   11.84  apply (erule OUN_E)
   11.85 -apply (drule ospec, assumption)
   11.86 -apply fast
   11.87 +apply (drule ospec, assumption, fast)
   11.88  apply (drule lemma4, assumption)
   11.89  apply (rule oallI)
   11.90  apply (rule impI)
   11.91 @@ -314,7 +308,7 @@
   11.92  apply (simp add: Union_recfunAC16_lesspoll)
   11.93  apply (rule Finite_lesspoll_infinite_Ord) 
   11.94  apply (rule Finite_def [THEN def_imp_iff, THEN iffD2]) 
   11.95 -apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption);  
   11.96 +apply (blast dest: ltD bij_is_fun [THEN apply_type], assumption)  
   11.97  apply (blast intro: Card_is_Ord) 
   11.98  done;
   11.99  
  11.100 @@ -528,7 +522,7 @@
  11.101  apply (erule imageE)
  11.102  apply (drule ltI, erule Limit_is_Ord) 
  11.103  apply (drule Limit_has_succ, assumption) 
  11.104 -apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption);
  11.105 +apply (frule_tac x1="succ(xa)" in spec [THEN mp], assumption)
  11.106  apply (erule conjE)
  11.107  apply (drule ospec) 
  11.108  (** LEVEL 10 **)
  11.109 @@ -559,8 +553,7 @@
  11.110  apply (rule allI)
  11.111  apply (rule impI)
  11.112  apply (frule WO2_infinite_subsets_eqpoll_X, assumption+)
  11.113 -apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp) 
  11.114 -apply simp 
  11.115 +apply (frule_tac n="k #+ m" in WO2_infinite_subsets_eqpoll_X, simp, simp) 
  11.116  apply (frule WO2_imp_ex_Card)
  11.117  apply (elim exE conjE)
  11.118  apply (drule eqpoll_trans [THEN eqpoll_sym, 
    12.1 --- a/src/ZF/AC/WO6_WO1.thy	Mon Jan 21 10:52:05 2002 +0100
    12.2 +++ b/src/ZF/AC/WO6_WO1.thy	Mon Jan 21 11:25:45 2002 +0100
    12.3 @@ -446,9 +446,7 @@
    12.4  (* ********************************************************************** *)
    12.5  
    12.6  lemma WO6_imp_NN_not_empty: "WO6 ==> NN(y) \<noteq> 0"
    12.7 -apply (unfold WO6_def NN_def, clarify) 
    12.8 -apply blast
    12.9 -done
   12.10 +by (unfold WO6_def NN_def, clarify, blast)
   12.11  
   12.12  (* ********************************************************************** *)
   12.13  (*      1 \<in> NN(y) ==> y can be well-ordered                               *)
    13.1 --- a/src/ZF/CardinalArith.thy	Mon Jan 21 10:52:05 2002 +0100
    13.2 +++ b/src/ZF/CardinalArith.thy	Mon Jan 21 11:25:45 2002 +0100
    13.3 @@ -45,8 +45,7 @@
    13.4  lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
    13.5  apply (erule trans_induct3 [of j])
    13.6  apply (simp_all add: oadd_Limit)
    13.7 -apply (simp add: Union_empty_iff Limit_def lt_def)
    13.8 -apply blast
    13.9 +apply (simp add: Union_empty_iff Limit_def lt_def, blast)
   13.10  done
   13.11  
   13.12  lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j"
   13.13 @@ -66,8 +65,7 @@
   13.14   apply (rule Ord_0_lt)
   13.15    apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
   13.16   apply (force simp add: Union_empty_iff oadd_eq_0_iff
   13.17 -                        Limit_is_Ord [of j, THEN Ord_in_Ord])
   13.18 -apply auto
   13.19 +                        Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
   13.20  apply (rule_tac x="succ(x)" in bexI)
   13.21   apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
   13.22  apply (simp add: Limit_def lt_def) 
   13.23 @@ -110,7 +108,7 @@
   13.24  apply (erule eqpollE)
   13.25  apply (rule succ_lepoll_natE)
   13.26  apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 
   13.27 -                    lepoll_trans, assumption); 
   13.28 +                    lepoll_trans, assumption) 
   13.29  done
   13.30  
   13.31  lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
   13.32 @@ -133,12 +131,12 @@
   13.33  apply (rule allI)
   13.34  apply (rule impI)
   13.35  apply (erule conjE)
   13.36 -apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], (assumption))
   13.37 -apply (frule Diff_sing_eqpoll, (assumption))
   13.38 +apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
   13.39 +apply (frule Diff_sing_eqpoll, assumption)
   13.40  apply (erule allE)
   13.41  apply (erule impE, fast)
   13.42 -apply (drule subsetD, (assumption))
   13.43 -apply (drule Fin.consI, (assumption))
   13.44 +apply (drule subsetD, assumption)
   13.45 +apply (drule Fin.consI, assumption)
   13.46  apply (simp add: cons_Diff)
   13.47  done
   13.48  
    14.1 --- a/src/ZF/Main.thy	Mon Jan 21 10:52:05 2002 +0100
    14.2 +++ b/src/ZF/Main.thy	Mon Jan 21 11:25:45 2002 +0100
    14.3 @@ -60,9 +60,9 @@
    14.4  (* belongs to theory CardinalArith *)
    14.5  
    14.6  lemma InfCard_square_eqpoll: "InfCard(K) \<Longrightarrow> K \<times> K \<approx> K"
    14.7 -apply (rule well_ord_InfCard_square_eq);  
    14.8 - apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]); 
    14.9 -apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]); 
   14.10 +apply (rule well_ord_InfCard_square_eq)  
   14.11 + apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) 
   14.12 +apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) 
   14.13  done
   14.14  
   14.15  lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)"
    15.1 --- a/src/ZF/OrdQuant.thy	Mon Jan 21 10:52:05 2002 +0100
    15.2 +++ b/src/ZF/OrdQuant.thy	Mon Jan 21 11:25:45 2002 +0100
    15.3 @@ -45,8 +45,7 @@
    15.4  lemma Union_upper_le:
    15.5       "\<lbrakk>j: J;  i\<le>j;  Ord(\<Union>(J))\<rbrakk> \<Longrightarrow> i \<le> \<Union>J"
    15.6  apply (subst Union_eq_UN)  
    15.7 -apply (rule UN_upper_le)
    15.8 -apply auto
    15.9 +apply (rule UN_upper_le, auto)
   15.10  done
   15.11  
   15.12  lemma zero_not_Limit [iff]: "~ Limit(0)"
   15.13 @@ -61,8 +60,7 @@
   15.14  done
   15.15  
   15.16  lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
   15.17 -apply (simp add: Limit_def lt_Ord2)
   15.18 -apply clarify
   15.19 +apply (simp add: Limit_def lt_Ord2, clarify)
   15.20  apply (drule_tac i=y in ltD) 
   15.21  apply (blast intro: lt_trans1 succ_leI ltI lt_Ord2)
   15.22  done
   15.23 @@ -115,8 +113,7 @@
   15.24  
   15.25  lemma OUN_upper_le:
   15.26       "\<lbrakk>a<A;  i\<le>b(a);  Ord(\<Union>x<A. b(x))\<rbrakk> \<Longrightarrow> i \<le> (\<Union>x<A. b(x))"
   15.27 -apply (unfold OUnion_def)
   15.28 -apply auto
   15.29 +apply (unfold OUnion_def, auto)
   15.30  apply (rule UN_upper_le )
   15.31  apply (auto simp add: lt_def) 
   15.32  done