# HG changeset patch
# User paulson
# Date 1011608745 -3600
# Node ID 02e2ff3e4d37baf091e48232b5c1792d0f22a41b
# Parent  2f61bca07de77beb5ed0754de816345a194c26fe
lexical tidying

diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/AC15_WO6.thy
--- a/src/ZF/AC/AC15_WO6.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC15_WO6.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -43,7 +43,7 @@
 apply (drule subset_consI [THEN subset_imp_lepoll, THEN lepoll_Finite])
 apply (rule nat_not_Finite [THEN notE] )
 apply (subgoal_tac "x ~= 0")
-apply (blast intro: lepoll_Sigma [THEN lepoll_Finite] , blast) 
+apply (blast intro: lepoll_Sigma [THEN lepoll_Finite], blast) 
 done
 
 lemma lemma1: "[| Union(C)=A; a \<in> A |] ==> \<exists>B \<in> C. a \<in> B & B \<subseteq> A"
@@ -61,8 +61,7 @@
 apply (unfold sets_of_size_between_def)
 apply (rule ballI)
 apply (erule_tac x="cons(0, B*nat)" in ballE)
- apply (blast dest: lemma1 intro!: lemma2) 
-apply blast
+ apply (blast dest: lemma1 intro!: lemma2, blast)
 done
 
 lemma lemma4: "[| A \<lesssim> i; Ord(i) |] ==> {P(a). a \<in> A} \<lesssim> i"
@@ -180,7 +179,7 @@
 apply (rule_tac x = "\<lambda>j \<in> (LEAST i. HH (f,A,i) ={A}) . HH (f,A,j) " in exI)
 apply simp
 apply (fast intro!: Ord_Least lam_type [THEN domain_of_fun]
-            elim!: less_Least_subset_x lemma1 lemma2, assumption); 
+            elim!: less_Least_subset_x lemma1 lemma2, assumption) 
 done
 
 
@@ -199,7 +198,7 @@
 theorem AC10_AC13: "[| n \<in> nat; 1\<le>n; AC10(n) |] ==> AC13(n)"
 apply (unfold AC10_def AC13_def, safe)
 apply (erule allE) 
-apply (erule impE [OF _ cons_times_nat_not_Finite], assumption); 
+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
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC16_WO4.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -144,7 +144,7 @@
 apply (erule impE)
 apply (simp add: add_succ)
 apply (fast intro!: Diff_sing_eqpoll lepoll_Diff_sing) 
-apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp); 
+apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
 apply blast 
 done
 
@@ -171,7 +171,7 @@
 apply (erule_tac x = "B - {xa}" in allE)
 apply (erule impE)
 apply (force intro: eqpoll_sym intro!: Diff_sing_eqpoll)
-apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp); 
+apply (subgoal_tac "A - {xa} - (B - {xa}) = A - B", simp)
 apply blast 
 done
 
@@ -361,7 +361,7 @@
 (** LEVEL 8 **)
 apply (rule w_Int_eqpoll_m [THEN eqpoll_m_not_empty, THEN not_emptyE])
 apply (blast, assumption+)
-apply (drule equalityD1 [THEN subsetD], (assumption))
+apply (drule equalityD1 [THEN subsetD], assumption)
 apply (frule cons_cons_in, assumption+)
 apply (blast dest: ex1_two_eq intro: s_subset [THEN subsetD] in_s_imp_u_in)+
 done
@@ -385,7 +385,7 @@
 apply (erule exE)
 apply (rule well_ord_subsets_eqpoll_n [THEN exE], assumption)
 apply (simp add: subsets_lepoll_succ)
-apply (drule well_ord_radd, (assumption))
+apply (drule well_ord_radd, assumption)
 apply (erule Int_empty [THEN disj_Un_eqpoll_sum,
                   THEN eqpoll_def [THEN def_imp_iff, THEN iffD1], THEN exE])
 apply (fast elim!: bij_is_inj [THEN well_ord_rvimage])
@@ -410,9 +410,8 @@
 
 lemma (in AC16) unique_superset_in_MM:
      "v \<in> LL ==> \<exists>! w. w \<in> MM & v \<subseteq> w"
-apply (unfold MM_def LL_def, safe)
-apply fast
-apply (rule lepoll_imp_eqpoll_subset [THEN exE], (assumption))
+apply (unfold MM_def LL_def, safe, fast)
+apply (rule lepoll_imp_eqpoll_subset [THEN exE], assumption)
 apply (rule_tac x = "x" in all_ex [THEN ballE]) 
 apply (blast intro: eqpoll_sym)+
 done
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/AC16_lemmas.thy
--- a/src/ZF/AC/AC16_lemmas.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC16_lemmas.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -40,8 +40,7 @@
 apply (fast intro!: RepFunI)
 apply (rule subsetI)
 apply (erule RepFunE)
-apply (rule CollectI)
-apply fast
+apply (rule CollectI, fast)
 apply (fast intro!: singleton_eqpoll_1)
 done
 
@@ -49,10 +48,8 @@
 apply (unfold eqpoll_def bij_def)
 apply (rule_tac x = "\<lambda>x \<in> X. {x}" in exI)
 apply (rule IntI)
-apply (unfold inj_def surj_def)
-apply simp
-apply (fast intro!: lam_type RepFunI intro: singleton_eq_iff [THEN iffD1])
-apply simp
+apply (unfold inj_def surj_def, simp)
+apply (fast intro!: lam_type RepFunI intro: singleton_eq_iff [THEN iffD1], simp)
 apply (fast intro!: lam_type)
 done
 
@@ -76,15 +73,15 @@
 apply (unfold lepoll_def)
 apply (rule_tac x = "\<lambda>y \<in> {y \<in> Pow(x) . y\<approx>succ (succ (n))}. 
                       <LEAST i. i \<in> y, y-{LEAST i. i \<in> y}>" in exI)
-apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective);
- apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in);
-apply (simp, blast intro: InfCard_Least_in);
+apply (rule_tac d = "%z. cons (fst(z), snd(z))" in lam_injective)
+ apply (blast intro!: Diff_sing_eqpoll intro: InfCard_Least_in)
+apply (simp, blast intro: InfCard_Least_in)
 done
 
 lemma set_of_Ord_succ_Union: "(\<forall>y \<in> z. Ord(y)) ==> z \<subseteq> succ(Union(z))"
 apply (rule subsetI)
-apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast );
-apply (simp, erule bexE); 
+apply (case_tac "\<forall>y \<in> z. y \<subseteq> x", blast )
+apply (simp, erule bexE) 
 apply (rule_tac i=xa and j=x in Ord_linear_le)
 apply (blast dest: le_imp_subset elim: leE ltE)+
 done
@@ -94,8 +91,7 @@
 
 lemma succ_Union_not_mem:
      "(!!y. y \<in> z ==> Ord(y)) ==> succ(Union(z)) \<notin> z"
-apply (rule set_of_Ord_succ_Union [THEN subset_not_mem]);
-apply blast
+apply (rule set_of_Ord_succ_Union [THEN subset_not_mem], blast)
 done
 
 lemma Union_cons_eq_succ_Union:
@@ -115,35 +111,31 @@
 apply (intro allI impI)
 apply (erule natE)
 apply (fast dest!: eqpoll_1_iff_singleton [THEN iffD1]
-            intro!: Union_singleton)
-apply (clarify ); 
+            intro!: Union_singleton, clarify) 
 apply (elim not_emptyE)
 apply (erule_tac x = "z-{xb}" in allE)
 apply (erule impE)
 apply (fast elim!: Diff_sing_eqpoll
                    Diff_sing_eqpoll [THEN eqpoll_succ_imp_not_empty])
-apply (subgoal_tac "xb \<union> \<Union>(z - {xb}) \<in> z");
-apply (simp add: Union_eq_Un [symmetric]);
+apply (subgoal_tac "xb \<union> \<Union>(z - {xb}) \<in> z")
+apply (simp add: Union_eq_Un [symmetric])
 apply (frule bspec, assumption)
-apply (drule bspec); 
-apply (erule Diff_subset [THEN subsetD]);
-apply (drule Un_Ord_disj, assumption)
-apply (auto ); 
+apply (drule bspec) 
+apply (erule Diff_subset [THEN subsetD])
+apply (drule Un_Ord_disj, assumption, auto) 
 done
 
 lemma Union_in: "[| \<forall>x \<in> z. Ord(x); z\<approx>n; z\<noteq>0; n \<in> nat |] ==> Union(z) \<in> z"
-apply (blast intro: Union_in_lemma); 
-done
+by (blast intro: Union_in_lemma)
 
 lemma succ_Union_in_x:
      "[| InfCard(x); z \<in> Pow(x); z\<approx>n; n \<in> nat |] ==> succ(Union(z)) \<in> x"
-apply (rule Limit_has_succ [THEN ltE]);
+apply (rule Limit_has_succ [THEN ltE])
 prefer 3 apply assumption
 apply (erule InfCard_is_Limit)
-apply (case_tac "z=0");
-apply (simp, fast intro!: InfCard_is_Limit [THEN Limit_has_0]);
-apply (rule ltI [OF PowD [THEN subsetD] InfCard_is_Card [THEN Card_is_Ord]]);
-apply assumption; 
+apply (case_tac "z=0")
+apply (simp, fast intro!: InfCard_is_Limit [THEN Limit_has_0])
+apply (rule ltI [OF PowD [THEN subsetD] InfCard_is_Card [THEN Card_is_Ord]], assumption)
 apply (blast intro: Union_in
                     InfCard_is_Card [THEN Card_is_Ord, THEN Ord_in_Ord])+
 done
@@ -151,18 +143,18 @@
 lemma succ_lepoll_succ_succ:
      "[| InfCard(x); n \<in> nat |] 
       ==> {y \<in> Pow(x). y\<approx>succ(n)} \<lesssim> {y \<in> Pow(x). y\<approx>succ(succ(n))}"
-apply (unfold lepoll_def);
+apply (unfold lepoll_def)
 apply (rule_tac x = "\<lambda>z \<in> {y\<in>Pow(x). y\<approx>succ(n)}. cons(succ(Union(z)), z)" 
        in exI)
 apply (rule_tac d = "%z. z-{Union (z) }" in lam_injective)
 apply (blast intro!: succ_Union_in_x succ_Union_not_mem
              intro: cons_eqpoll_succ Ord_in_Ord
              dest!: InfCard_is_Card [THEN Card_is_Ord])
-apply (simp only: Union_cons_eq_succ_Union); 
-apply (rule cons_Diff_eq);
+apply (simp only: Union_cons_eq_succ_Union) 
+apply (rule cons_Diff_eq)
 apply (fast dest!: InfCard_is_Card [THEN Card_is_Ord]
             elim: Ord_in_Ord 
-            intro!: succ_Union_not_mem);
+            intro!: succ_Union_not_mem)
 done
 
 lemma subsets_eqpoll_X:
@@ -170,9 +162,9 @@
 apply (induct_tac "n")
 apply (rule subsets_eqpoll_1_eqpoll)
 apply (rule eqpollI)
-apply (rule subsets_lepoll_lemma1 [THEN lepoll_trans], assumption+);
-apply (rule eqpoll_trans [THEN eqpoll_imp_lepoll]); 
- apply (erule eqpoll_refl [THEN prod_eqpoll_cong]);
+apply (rule subsets_lepoll_lemma1 [THEN lepoll_trans], assumption+)
+apply (rule eqpoll_trans [THEN eqpoll_imp_lepoll]) 
+ apply (erule eqpoll_refl [THEN prod_eqpoll_cong])
 apply (erule InfCard_square_eqpoll)
 apply (fast elim: eqpoll_sym [THEN eqpoll_imp_lepoll, THEN lepoll_trans] 
             intro!: succ_lepoll_succ_succ)
@@ -185,8 +177,7 @@
 done
 
 lemma vimage_image_eq: "[| f \<in> inj(A,B); y \<subseteq> A |] ==> converse(f)``(f``y) = y"
-apply (fast elim!: inj_is_fun [THEN apply_Pair] dest: inj_equality)
-done
+by (fast elim!: inj_is_fun [THEN apply_Pair] dest: inj_equality)
 
 lemma subsets_eqpoll:
      "A\<approx>B ==> {Y \<in> Pow(A). Y\<approx>n}\<approx>{Y \<in> Pow(B). Y\<approx>n}"
@@ -222,10 +213,10 @@
 lemma WO2_infinite_subsets_eqpoll_X: "[| WO2; n \<in> nat; ~Finite(X) |]   
         ==> {Y \<in> Pow(X). Y\<approx>succ(n)}\<approx>X"
 apply (drule WO2_imp_ex_Card)
-apply (elim allE exE conjE);
+apply (elim allE exE conjE)
 apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
 apply (drule infinite_Card_is_InfCard, assumption)
-apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans); 
+apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans) 
 done
 
 lemma well_ord_imp_ex_Card: "well_ord(X,R) ==> \<exists>a. Card(a) & X\<approx>a"
@@ -238,7 +229,7 @@
 apply (elim allE exE conjE)
 apply (frule eqpoll_imp_lepoll [THEN lepoll_infinite], assumption)
 apply (drule infinite_Card_is_InfCard, assumption)
-apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans); 
+apply (blast intro: subsets_eqpoll subsets_eqpoll_X eqpoll_sym eqpoll_trans) 
 done
 
 end
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/AC18_AC19.thy
--- a/src/ZF/AC/AC18_AC19.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC18_AC19.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -66,7 +66,7 @@
 
 lemma lemma1_1: "[|c \<in> a; x = c Un {0}; x \<notin> a |] ==> x - {0} \<in> a"
 apply clarify 
-apply (rule subst_elem , (assumption))
+apply (rule subst_elem, assumption)
 apply (fast elim: notE subst_elem)
 done
 
@@ -98,10 +98,9 @@
 apply (case_tac "A=0", force)
 apply (erule_tac x = "{uu (a) . a \<in> A}" in allE)
 apply (erule impE)
-apply (erule RepRep_conj , (assumption))
+apply (erule RepRep_conj, assumption)
 apply (rule lemma1)
-apply (drule lemma2 , (assumption))
-apply auto 
+apply (drule lemma2, assumption, auto) 
 done
 
 end
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -139,7 +139,7 @@
 apply (unfold rvimage_def)
 apply (rule equalityI, safe)
 apply (drule_tac P = "%a. <id (A) `xb,a>:r" in id_conv [THEN subst],
-       (assumption))
+       assumption)
 apply (drule_tac P = "%a. <a,ya>:r" in id_conv [THEN subst], (assumption+))
 apply (fast intro: id_conv [THEN ssubst])
 done
@@ -179,7 +179,7 @@
 lemma surj_image_eq: "f \<in> surj(A, B) ==> f``A = B"
 apply (unfold surj_def)
 apply (erule CollectE)
-apply (rule image_fun [THEN ssubst], (assumption), rule subset_refl)
+apply (rule image_fun [THEN ssubst], assumption, rule subset_refl)
 apply (blast dest: apply_type) 
 done
 
@@ -217,7 +217,7 @@
 apply (fast intro: LeastI2 nat_into_Ord [THEN Ord_in_Ord] 
                            inj_is_fun [THEN apply_type])
 apply (erule domainE)
-apply (frule inj_is_fun [THEN apply_type], (assumption))
+apply (frule inj_is_fun [THEN apply_type], assumption)
 apply (rule LeastI2)
 apply (auto elim!: nat_into_Ord [THEN Ord_in_Ord])
 done
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/Cardinal_aux.thy
--- a/src/ZF/AC/Cardinal_aux.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/Cardinal_aux.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -8,7 +8,7 @@
 theory Cardinal_aux = AC_Equiv:
 
 lemma Diff_lepoll: "[| A \<lesssim> succ(m); B \<subseteq> A; B\<noteq>0 |] ==> A-B \<lesssim> m"
-apply (rule not_emptyE, (assumption))
+apply (rule not_emptyE, assumption)
 apply (blast intro: lepoll_trans [OF subset_imp_lepoll Diff_sing_lepoll])
 done
 
@@ -151,7 +151,7 @@
          ~Finite(a); Ord(a); n \<in> nat |] 
       ==> (\<Union>b \<in> a. F(b)) \<lesssim> a"
 apply (rule rev_mp) 
-apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll);
+apply (rule_tac f="\<lambda>b \<in> a. F (b)" in UN_fun_lepoll)
 apply auto
 done
 
@@ -187,7 +187,7 @@
 apply (drule Un_least_lt, assumption)
 apply (drule eqpoll_imp_lepoll [THEN lepoll_trans], 
        rule le_imp_lepoll, assumption)+
-apply (case_tac "Finite(x Un xa)");
+apply (case_tac "Finite(x Un xa)")
 txt{*finite case*}
  apply (drule Finite_Un [OF lepoll_Finite lepoll_Finite], assumption+) 
  apply (drule subset_Un_Diff [THEN subset_imp_lepoll, THEN lepoll_Finite])
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/DC.thy
--- a/src/ZF/AC/DC.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/DC.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -363,8 +363,7 @@
 apply (unfold XX_def)
 apply (drule apply_type, assumption)
 apply (elim UN_E CollectE)
-apply (drule domain_of_fun [symmetric, THEN trans], assumption)
-apply simp
+apply (drule domain_of_fun [symmetric, THEN trans], assumption, simp)
 done
 
 lemma (in imp_DC0) restrict_cons_eq_restrict: 
@@ -404,7 +403,7 @@
 (*induction step*) (** LEVEL 5 **)
 (*prevent simplification of ~\<exists> to \<forall>~ *)
 apply (simp only: separation split)
-apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI);
+apply (drule_tac x="succ(xa)" in ospec, blast intro: ltI)
 apply (elim conjE disjE)
 apply (force elim!: trans subst_context
              intro!: UN_image_succ_eq_succ)
@@ -455,8 +454,7 @@
 apply (frule lemma2 [THEN conjunct1, THEN domain_of_fun], assumption+)
 apply (unfold allRR_def)
 apply (drule ospec) 
-apply (drule ltI [OF nat_succI Ord_nat], assumption)
-apply simp
+apply (drule ltI [OF nat_succI Ord_nat], assumption, simp)
 apply (elim conjE ballE)
 apply (erule restrict_eq_imp_val_eq [symmetric], force) 
 apply (simp add: image_fun OrdmemD) 
@@ -500,7 +498,7 @@
 theorem DC_WO3: "(\<forall>K. Card(K) --> DC(K)) ==> WO3"
 apply (unfold DC_def WO3_def)
 apply (rule allI)
-apply (case_tac "A \<prec> Hartog (A)");
+apply (case_tac "A \<prec> Hartog (A)")
 apply (fast dest!: lesspoll_imp_ex_lt_eqpoll 
             intro!: Ord_Hartog leI [THEN le_imp_subset])
 apply (erule allE impE)+
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/HH.thy
--- a/src/ZF/AC/HH.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/HH.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -239,8 +239,7 @@
 apply (rule bij_Least_HH_x [THEN bij_converse_bij])
 apply (rule f_subsets_imp_UN_HH_eq_x)
 apply (intro ballI apply_type) 
-apply (fast intro: lam_type apply_type del: DiffE)
-apply assumption; 
+apply (fast intro: lam_type apply_type del: DiffE, assumption) 
 apply (fast intro: Pi_weaken_type)
 done
 
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/Hartog.thy
--- a/src/ZF/AC/Hartog.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/Hartog.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -25,7 +25,7 @@
   apply (erule inj_is_fun [THEN fun_is_rel, THEN image_subset])
  apply (rule well_ord_rvimage [OF bij_is_inj well_ord_Memrel]) 
   apply (erule restrict_bij [THEN bij_converse_bij]) 
-apply (rule subset_refl, assumption); 
+apply (rule subset_refl, assumption) 
 apply (rule trans) 
 apply (rule bij_ordertype_vimage) 
 apply (erule restrict_bij [THEN bij_converse_bij]) 
@@ -36,8 +36,7 @@
 
 lemma Ord_lepoll_imp_eq_ordertype:
      "[| Ord(a); a \<lesssim> X |] ==> \<exists>Y. Y \<subseteq> X & (\<exists>R. R \<subseteq> X*X & ordertype(Y,R)=a)"
-apply (drule Ord_lepoll_imp_ex_well_ord, (assumption))
-apply clarify
+apply (drule Ord_lepoll_imp_ex_well_ord, assumption, clarify)
 apply (intro exI conjI)
 apply (erule_tac [3] ordertype_Int, auto) 
 done
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/WO1_WO7.thy
--- a/src/ZF/AC/WO1_WO7.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/WO1_WO7.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -50,7 +50,7 @@
 lemma converse_Memrel_not_wf_on: 
     "[| Ord(a); ~Finite(a) |] ==> ~wf[a](converse(Memrel(a)))"
 apply (unfold wf_on_def wf_def)
-apply (drule nat_le_infinite_Ord [THEN le_imp_subset], (assumption))
+apply (drule nat_le_infinite_Ord [THEN le_imp_subset], assumption)
 apply (rule notI)
 apply (erule_tac x = "nat" in allE, blast)
 done
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/WO2_AC16.thy
--- a/src/ZF/AC/WO2_AC16.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/WO2_AC16.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -31,8 +31,7 @@
 (* ********************************************************************** *)
 
 lemma recfunAC16_0: "recfunAC16(f,h,0,a) = 0"
-apply (simp add: recfunAC16_def);
-done
+by (simp add: recfunAC16_def)
 
 lemma recfunAC16_succ: 
      "recfunAC16(f,h,succ(i),a) =   
@@ -41,7 +40,7 @@
             {f ` (LEAST j. h ` i \<subseteq> f ` j &   
              (\<forall>b<a. (h`b \<subseteq> f`j   
               --> (\<forall>t \<in> recfunAC16(f,h,i,a). ~ h`b \<subseteq> t))))})"
-apply (simp add: recfunAC16_def);
+apply (simp add: recfunAC16_def)
 done
 
 lemma recfunAC16_Limit: "Limit(i)   
@@ -55,12 +54,11 @@
 lemma transrec2_mono_lemma [rule_format]:
      "[| !!g r. r \<subseteq> B(g,r);  Ord(i) |]   
       ==> j<i --> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
-apply (erule trans_induct);
-apply (rule Ord_cases , assumption+);
-apply fast
+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 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
@@ -68,9 +66,9 @@
 lemma transrec2_mono:
      "[| !!g r. r \<subseteq> B(g,r); j\<le>i |] 
       ==> transrec2(j, 0, B) \<subseteq> transrec2(i, 0, B)"
-apply (erule leE);
+apply (erule leE)
 apply (rule transrec2_mono_lemma)
-apply (auto intro: lt_Ord2 ); 
+apply (auto intro: lt_Ord2 ) 
 done
 
 (* ********************************************************************** *)
@@ -80,8 +78,7 @@
 lemma recfunAC16_mono: 
        "i\<le>j ==> recfunAC16(f, g, i, a) \<subseteq> recfunAC16(f, g, j, a)"
 apply (unfold recfunAC16_def)
-apply (rule transrec2_mono)
-apply (auto ); 
+apply (rule transrec2_mono, auto) 
 done
 
 (* ********************************************************************** *)
@@ -95,8 +92,7 @@
         V \<in> F(i); f(z)<=V; W \<in> F(j); f(z)<=W |]   
      ==> V = W"
 apply (erule asm_rl allE impE)+
-apply (drule subsetD, assumption)
-apply blast 
+apply (drule subsetD, assumption, blast) 
 done
 
 
@@ -118,8 +114,7 @@
       ==> \<forall>y<x. \<forall>z<a. z < y | (\<exists>Y \<in> F(y). h(z) \<subseteq> Y) -->   
                        (\<exists>! Y. Y \<in> F(y) & h(z) \<subseteq> Y)"
 apply (intro oallI impI)
-apply (drule ospec, assumption)
-apply clarify
+apply (drule ospec, assumption, clarify)
 apply (blast elim!: oallE ) 
 done
 
@@ -134,8 +129,7 @@
 apply (rule conjI)
 apply (rule subsetI)
 apply (erule OUN_E)
-apply (drule ospec, assumption)
-apply fast
+apply (drule ospec, assumption, fast)
 apply (drule lemma4, assumption)
 apply (rule oallI)
 apply (rule impI)
@@ -314,7 +308,7 @@
 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 dest: ltD bij_is_fun [THEN apply_type], assumption)  
 apply (blast intro: Card_is_Ord) 
 done;
 
@@ -528,7 +522,7 @@
 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 (frule_tac x1="succ(xa)" in spec [THEN mp], assumption)
 apply (erule conjE)
 apply (drule ospec) 
 (** LEVEL 10 **)
@@ -559,8 +553,7 @@
 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) 
-apply simp 
+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, 
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/AC/WO6_WO1.thy
--- a/src/ZF/AC/WO6_WO1.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/AC/WO6_WO1.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -446,9 +446,7 @@
 (* ********************************************************************** *)
 
 lemma WO6_imp_NN_not_empty: "WO6 ==> NN(y) \<noteq> 0"
-apply (unfold WO6_def NN_def, clarify) 
-apply blast
-done
+by (unfold WO6_def NN_def, clarify, blast)
 
 (* ********************************************************************** *)
 (*      1 \<in> NN(y) ==> y can be well-ordered                               *)
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/CardinalArith.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -45,8 +45,7 @@
 lemma oadd_eq_0_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> (i ++ j) = 0 <-> i=0 & j=0"
 apply (erule trans_induct3 [of j])
 apply (simp_all add: oadd_Limit)
-apply (simp add: Union_empty_iff Limit_def lt_def)
-apply blast
+apply (simp add: Union_empty_iff Limit_def lt_def, blast)
 done
 
 lemma oadd_eq_lt_iff: "\<lbrakk>Ord(i); Ord(j)\<rbrakk> \<Longrightarrow> 0 < (i ++ j) <-> 0<i | 0<j"
@@ -66,8 +65,7 @@
  apply (rule Ord_0_lt)
   apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
  apply (force simp add: Union_empty_iff oadd_eq_0_iff
-                        Limit_is_Ord [of j, THEN Ord_in_Ord])
-apply auto
+                        Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
 apply (rule_tac x="succ(x)" in bexI)
  apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
 apply (simp add: Limit_def lt_def) 
@@ -110,7 +108,7 @@
 apply (erule eqpollE)
 apply (rule succ_lepoll_natE)
 apply (blast intro: nat_succI [THEN OrdmemD, THEN subset_imp_lepoll] 
-                    lepoll_trans, assumption); 
+                    lepoll_trans, assumption) 
 done
 
 lemma in_Card_imp_lesspoll: "[| Card(K); b \<in> K |] ==> b \<prec> K"
@@ -133,12 +131,12 @@
 apply (rule allI)
 apply (rule impI)
 apply (erule conjE)
-apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], (assumption))
-apply (frule Diff_sing_eqpoll, (assumption))
+apply (rule eqpoll_succ_imp_not_empty [THEN not_emptyE], assumption)
+apply (frule Diff_sing_eqpoll, assumption)
 apply (erule allE)
 apply (erule impE, fast)
-apply (drule subsetD, (assumption))
-apply (drule Fin.consI, (assumption))
+apply (drule subsetD, assumption)
+apply (drule Fin.consI, assumption)
 apply (simp add: cons_Diff)
 done
 
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/Main.thy
--- a/src/ZF/Main.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/Main.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -60,9 +60,9 @@
 (* belongs to theory CardinalArith *)
 
 lemma InfCard_square_eqpoll: "InfCard(K) \<Longrightarrow> K \<times> K \<approx> K"
-apply (rule well_ord_InfCard_square_eq);  
- apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]); 
-apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]); 
+apply (rule well_ord_InfCard_square_eq)  
+ apply (erule InfCard_is_Card [THEN Card_is_Ord, THEN well_ord_Memrel]) 
+apply (simp add: InfCard_is_Card [THEN Card_cardinal_eq]) 
 done
 
 lemma Inf_Card_is_InfCard: "[| ~Finite(i); Card(i) |] ==> InfCard(i)"
diff -r 2f61bca07de7 -r 02e2ff3e4d37 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Mon Jan 21 10:52:05 2002 +0100
+++ b/src/ZF/OrdQuant.thy	Mon Jan 21 11:25:45 2002 +0100
@@ -45,8 +45,7 @@
 lemma Union_upper_le:
      "\<lbrakk>j: J;  i\<le>j;  Ord(\<Union>(J))\<rbrakk> \<Longrightarrow> i \<le> \<Union>J"
 apply (subst Union_eq_UN)  
-apply (rule UN_upper_le)
-apply auto
+apply (rule UN_upper_le, auto)
 done
 
 lemma zero_not_Limit [iff]: "~ Limit(0)"
@@ -61,8 +60,7 @@
 done
 
 lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
-apply (simp add: Limit_def lt_Ord2)
-apply clarify
+apply (simp add: Limit_def lt_Ord2, clarify)
 apply (drule_tac i=y in ltD) 
 apply (blast intro: lt_trans1 succ_leI ltI lt_Ord2)
 done
@@ -115,8 +113,7 @@
 
 lemma OUN_upper_le:
      "\<lbrakk>a<A;  i\<le>b(a);  Ord(\<Union>x<A. b(x))\<rbrakk> \<Longrightarrow> i \<le> (\<Union>x<A. b(x))"
-apply (unfold OUnion_def)
-apply auto
+apply (unfold OUnion_def, auto)
 apply (rule UN_upper_le )
 apply (auto simp add: lt_def) 
 done