tidying (by script)
authorpaulson
Thu Jan 23 10:30:14 2003 +0100 (2003-01-23 ago)
changeset 13784b9f6154427a4
parent 13783 3294f727e20d
child 13785 e2fcd88be55d
tidying (by script)
src/ZF/Arith.thy
src/ZF/ArithSimp.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Epsilon.thy
src/ZF/Finite.thy
src/ZF/List.thy
src/ZF/Nat.thy
src/ZF/OrderArith.thy
src/ZF/Ordinal.thy
src/ZF/Perm.thy
src/ZF/QPair.thy
src/ZF/Trancl.thy
src/ZF/Univ.thy
src/ZF/WF.thy
src/ZF/Zorn.thy
     1.1 --- a/src/ZF/Arith.thy	Thu Jan 23 09:16:53 2003 +0100
     1.2 +++ b/src/ZF/Arith.thy	Thu Jan 23 10:30:14 2003 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4  (*Must simplify BEFORE the induction: else we get a critical pair*)
     1.5  lemma diff_succ_succ [simp]: "succ(m) #- succ(n) = m #- n"
     1.6  apply (simp add: natify_succ diff_def)
     1.7 -apply (rule_tac x1 = "n" in natify_in_nat [THEN nat_induct], auto)
     1.8 +apply (rule_tac x1 = n in natify_in_nat [THEN nat_induct], auto)
     1.9  done
    1.10  
    1.11  (*This defining property is no longer wanted*)
    1.12 @@ -212,7 +212,7 @@
    1.13  
    1.14  lemma diff_le_self: "m:nat ==> (m #- n) le m"
    1.15  apply (subgoal_tac " (m #- natify (n)) le m")
    1.16 -apply (rule_tac [2] m = "m" and n = "natify (n) " in diff_induct)
    1.17 +apply (rule_tac [2] m = m and n = "natify (n) " in diff_induct)
    1.18  apply (erule_tac [6] leE)
    1.19  apply (simp_all add: le_iff)
    1.20  done
    1.21 @@ -528,7 +528,7 @@
    1.22  
    1.23  lemma less_diff_conv [rule_format]:
    1.24       "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"
    1.25 -by (erule_tac m = "k" in diff_induct, auto)
    1.26 +by (erule_tac m = k in diff_induct, auto)
    1.27  
    1.28  lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
    1.29  
     2.1 --- a/src/ZF/ArithSimp.thy	Thu Jan 23 09:16:53 2003 +0100
     2.2 +++ b/src/ZF/ArithSimp.thy	Thu Jan 23 10:30:14 2003 +0100
     2.3 @@ -24,7 +24,7 @@
     2.4  lemma add_diff_inverse: "[| n le m;  m:nat |] ==> n #+ (m#-n) = m"
     2.5  apply (frule lt_nat_in_nat, erule nat_succI)
     2.6  apply (erule rev_mp)
     2.7 -apply (rule_tac m = "m" and n = "n" in diff_induct, auto)
     2.8 +apply (rule_tac m = m and n = n in diff_induct, auto)
     2.9  done
    2.10  
    2.11  lemma add_diff_inverse2: "[| n le m;  m:nat |] ==> (m#-n) #+ n = m"
    2.12 @@ -36,13 +36,13 @@
    2.13  lemma diff_succ: "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)"
    2.14  apply (frule lt_nat_in_nat, erule nat_succI)
    2.15  apply (erule rev_mp)
    2.16 -apply (rule_tac m = "m" and n = "n" in diff_induct)
    2.17 +apply (rule_tac m = m and n = n in diff_induct)
    2.18  apply (simp_all (no_asm_simp))
    2.19  done
    2.20  
    2.21  lemma zero_less_diff [simp]:
    2.22       "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n"
    2.23 -apply (rule_tac m = "m" and n = "n" in diff_induct)
    2.24 +apply (rule_tac m = m and n = n in diff_induct)
    2.25  apply (simp_all (no_asm_simp))
    2.26  done
    2.27  
    2.28 @@ -67,7 +67,7 @@
    2.29  apply (frule lt_nat_in_nat, erule nat_succI)
    2.30  apply (erule rev_mp)
    2.31  apply (erule rev_mp)
    2.32 -apply (rule_tac m = "m" and n = "n" in diff_induct)
    2.33 +apply (rule_tac m = m and n = n in diff_induct)
    2.34  apply (simp_all (no_asm_simp) add: diff_le_self)
    2.35  done
    2.36  
    2.37 @@ -236,7 +236,7 @@
    2.38  done
    2.39  
    2.40  lemma mod_1_eq [simp]: "m mod 1 = 0"
    2.41 -by (cut_tac n = "1" in mod_less_divisor, auto)
    2.42 +by (cut_tac n = 1 in mod_less_divisor, auto)
    2.43  
    2.44  lemma mod2_cases: "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"
    2.45  apply (subgoal_tac "k mod 2: 2")
    2.46 @@ -257,7 +257,7 @@
    2.47  done
    2.48  
    2.49  lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0"
    2.50 -by (cut_tac n = "0" in mod2_add_more, auto)
    2.51 +by (cut_tac n = 0 in mod2_add_more, auto)
    2.52  
    2.53  
    2.54  subsection{*Additional theorems about @{text "\<le>"}*}
    2.55 @@ -368,7 +368,7 @@
    2.56  done
    2.57  
    2.58  lemma mult_le_cancel_le1: "k : nat ==> k #* m le k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) le 1)"
    2.59 -by (cut_tac k = "k" and m = "m" and n = "1" in mult_le_cancel1, auto)
    2.60 +by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto)
    2.61  
    2.62  lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)"
    2.63  by (blast intro: le_anti_sym)
    2.64 @@ -395,7 +395,7 @@
    2.65  
    2.66  lemma div_cancel_raw:
    2.67       "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n"
    2.68 -apply (erule_tac i = "m" in complete_induct)
    2.69 +apply (erule_tac i = m in complete_induct)
    2.70  apply (case_tac "x<n")
    2.71   apply (simp add: div_less zero_lt_mult_iff mult_lt_mono2)
    2.72  apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
    2.73 @@ -419,7 +419,7 @@
    2.74  apply (case_tac "n=0")
    2.75   apply (simp add: DIVISION_BY_ZERO_MOD)
    2.76  apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])
    2.77 -apply (erule_tac i = "m" in complete_induct)
    2.78 +apply (erule_tac i = m in complete_induct)
    2.79  apply (case_tac "x<n")
    2.80   apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2)
    2.81  apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono] 
    2.82 @@ -499,7 +499,7 @@
    2.83  
    2.84  lemma diff_is_0_lemma:
    2.85       "[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n"
    2.86 -apply (rule_tac m = "m" and n = "n" in diff_induct, simp_all)
    2.87 +apply (rule_tac m = m and n = n in diff_induct, simp_all)
    2.88  done
    2.89  
    2.90  lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) le natify(n)"
    2.91 @@ -514,8 +514,7 @@
    2.92        (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))"
    2.93  apply (case_tac "a < b")
    2.94   apply (force simp add: nat_lt_imp_diff_eq_0)
    2.95 -apply (rule iffI, force) 
    2.96 -apply simp 
    2.97 +apply (rule iffI, force, simp) 
    2.98  apply (drule_tac x="a#-b" in bspec)
    2.99  apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) 
   2.100  done
     3.1 --- a/src/ZF/Cardinal.thy	Thu Jan 23 09:16:53 2003 +0100
     3.2 +++ b/src/ZF/Cardinal.thy	Thu Jan 23 10:30:14 2003 +0100
     3.3 @@ -495,7 +495,7 @@
     3.4  apply (induct_tac m)
     3.5  apply (blast intro!: nat_0_le)
     3.6  apply (rule ballI)
     3.7 -apply (erule_tac n = "n" in natE)
     3.8 +apply (erule_tac n = n in natE)
     3.9  apply (simp (no_asm_simp) add: lepoll_def inj_def)
    3.10  apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
    3.11  done
    3.12 @@ -859,7 +859,7 @@
    3.13  apply (rule Diff_sing_eqpoll [THEN revcut_rl])
    3.14  prefer 2 apply assumption
    3.15  apply assumption
    3.16 -apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
    3.17 +apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
    3.18  apply (rule Fin.consI, blast)
    3.19  apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
    3.20  (*Now for the lemma assumed above*)
    3.21 @@ -907,7 +907,7 @@
    3.22  apply (subgoal_tac [2] "A-{a}=A", auto)
    3.23  apply (rule_tac x = "succ (n) " in bexI)
    3.24  apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
    3.25 -apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
    3.26 +apply (drule_tac a = a and b = n in cons_eqpoll_cong)
    3.27  apply (auto dest: mem_irrefl)
    3.28  done
    3.29  
    3.30 @@ -976,7 +976,7 @@
    3.31   apply (drule_tac x = x in bspec, assumption)
    3.32   apply (blast elim: mem_irrefl mem_asym)
    3.33  txt{*other case*} 
    3.34 -apply (drule_tac x = "Z" in spec, blast) 
    3.35 +apply (drule_tac x = Z in spec, blast) 
    3.36  done
    3.37  
    3.38  lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
     4.1 --- a/src/ZF/CardinalArith.thy	Thu Jan 23 09:16:53 2003 +0100
     4.2 +++ b/src/ZF/CardinalArith.thy	Thu Jan 23 10:30:14 2003 +0100
     4.3 @@ -585,14 +585,14 @@
     4.4  (*??WHAT A MESS!*)  
     4.5  apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1],
     4.6         (assumption | rule refl | erule ltI)+) 
     4.7 -apply (rule_tac i = "xa Un ya" and j = "nat" in Ord_linear2,
     4.8 +apply (rule_tac i = "xa Un ya" and j = nat in Ord_linear2,
     4.9         simp_all add: Ord_Un Ord_nat)
    4.10  prefer 2 (*case nat le (xa Un ya) *)
    4.11   apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] 
    4.12                    le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un
    4.13                  ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD])
    4.14  (*the finite case: xa Un ya < nat *)
    4.15 -apply (rule_tac j = "nat" in lt_trans2)
    4.16 +apply (rule_tac j = nat in lt_trans2)
    4.17   apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type
    4.18                    nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)
    4.19  apply (simp add: InfCard_def)
    4.20 @@ -645,7 +645,7 @@
    4.21  
    4.22  (*Corollary 10.13 (1), for cardinal multiplication*)
    4.23  lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K |*| L = K Un L"
    4.24 -apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
    4.25 +apply (rule_tac i = K and j = L in Ord_linear_le)
    4.26  apply (typecheck add: InfCard_is_Card Card_is_Ord)
    4.27  apply (rule cmult_commute [THEN ssubst])
    4.28  apply (rule Un_commute [THEN ssubst])
    4.29 @@ -669,7 +669,7 @@
    4.30  done
    4.31  
    4.32  lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L"
    4.33 -apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
    4.34 +apply (rule_tac i = K and j = L in Ord_linear_le)
    4.35  apply (typecheck add: InfCard_is_Card Card_is_Ord)
    4.36  apply (rule cadd_commute [THEN ssubst])
    4.37  apply (rule Un_commute [THEN ssubst])
    4.38 @@ -812,7 +812,7 @@
    4.39  
    4.40  lemma Finite_imp_succ_cardinal_Diff:
    4.41       "[| Finite(A);  a:A |] ==> succ(|A-{a}|) = |A|"
    4.42 -apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
    4.43 +apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
    4.44  apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
    4.45  apply (simp add: cons_Diff)
    4.46  done
     5.1 --- a/src/ZF/Cardinal_AC.thy	Thu Jan 23 09:16:53 2003 +0100
     5.2 +++ b/src/ZF/Cardinal_AC.thy	Thu Jan 23 10:30:14 2003 +0100
     5.3 @@ -83,7 +83,7 @@
     5.4  lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"
     5.5  apply (unfold surj_def)
     5.6  apply (erule CollectE)
     5.7 -apply (rule_tac A1 = "Y" and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
     5.8 +apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
     5.9  apply (fast elim!: apply_Pair)
    5.10  apply (blast dest: apply_type Pi_memberD 
    5.11               intro: apply_equality Pi_type f_imp_injective)
     6.1 --- a/src/ZF/Epsilon.thy	Thu Jan 23 09:16:53 2003 +0100
     6.2 +++ b/src/ZF/Epsilon.thy	Thu Jan 23 10:30:14 2003 +0100
     6.3 @@ -180,7 +180,7 @@
     6.4  lemma transrec_type:
     6.5      "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x) |]
     6.6       ==> transrec(a,H) : B(a)"
     6.7 -apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct])
     6.8 +apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct])
     6.9  apply (subst transrec)
    6.10  apply (simp add: lam_type) 
    6.11  done
    6.12 @@ -220,7 +220,7 @@
    6.13  by (subst rank_def [THEN def_transrec], simp)
    6.14  
    6.15  lemma Ord_rank [simp]: "Ord(rank(a))"
    6.16 -apply (rule_tac a="a" in eps_induct) 
    6.17 +apply (rule_tac a=a in eps_induct) 
    6.18  apply (subst rank)
    6.19  apply (rule Ord_succ [THEN Ord_UN])
    6.20  apply (erule bspec, assumption)
    6.21 @@ -233,7 +233,7 @@
    6.22  done
    6.23  
    6.24  lemma rank_lt: "a:b ==> rank(a) < rank(b)"
    6.25 -apply (rule_tac a1 = "b" in rank [THEN ssubst])
    6.26 +apply (rule_tac a1 = b in rank [THEN ssubst])
    6.27  apply (erule UN_I [THEN ltI])
    6.28  apply (rule_tac [2] Ord_UN, auto)
    6.29  done
     7.1 --- a/src/ZF/Finite.thy	Thu Jan 23 09:16:53 2003 +0100
     7.2 +++ b/src/ZF/Finite.thy	Thu Jan 23 10:30:14 2003 +0100
     7.3 @@ -90,7 +90,7 @@
     7.4  apply (erule Fin_induct)
     7.5  apply (simp add: subset_empty_iff)
     7.6  apply (simp add: subset_cons_iff distrib_simps, safe)
     7.7 -apply (erule_tac b = "z" in cons_Diff [THEN subst], simp)
     7.8 +apply (erule_tac b = z in cons_Diff [THEN subst], simp)
     7.9  done
    7.10  
    7.11  lemma Fin_subset: "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)"
    7.12 @@ -158,7 +158,7 @@
    7.13  apply (erule FiniteFun.induct)
    7.14  apply (simp add: subset_empty_iff FiniteFun.intros)
    7.15  apply (simp add: subset_cons_iff distrib_simps, safe)
    7.16 -apply (erule_tac b = "z" in cons_Diff [THEN subst])
    7.17 +apply (erule_tac b = z in cons_Diff [THEN subst])
    7.18  apply (drule spec [THEN mp], assumption)
    7.19  apply (fast intro!: FiniteFun.intros)
    7.20  done
     8.1 --- a/src/ZF/List.thy	Thu Jan 23 09:16:53 2003 +0100
     8.2 +++ b/src/ZF/List.thy	Thu Jan 23 10:30:14 2003 +0100
     8.3 @@ -354,8 +354,7 @@
     8.4  
     8.5  lemma drop_length [rule_format]:
     8.6       "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
     8.7 -apply (erule list.induct, simp_all)
     8.8 -apply safe
     8.9 +apply (erule list.induct, simp_all, safe)
    8.10  apply (erule drop_length_Cons)
    8.11  apply (rule natE)
    8.12  apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
    8.13 @@ -1121,8 +1120,7 @@
    8.14  lemma nth_map_upt [rule_format]:
    8.15       "[| m:nat; n:nat |] ==>
    8.16        \<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
    8.17 -apply (rule_tac n = m and m = n in diff_induct, typecheck, simp) 
    8.18 -apply simp 
    8.19 +apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp) 
    8.20  apply (subst map_succ_upt [symmetric], simp_all, clarify) 
    8.21  apply (subgoal_tac "i < length (upt (0, x))")
    8.22   prefer 2 
     9.1 --- a/src/ZF/Nat.thy	Thu Jan 23 09:16:53 2003 +0100
     9.2 +++ b/src/ZF/Nat.thy	Thu Jan 23 10:30:14 2003 +0100
     9.3 @@ -174,7 +174,7 @@
     9.4          !!y. y: nat ==> P(0,succ(y));   
     9.5          !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
     9.6       ==> P(m,n)"
     9.7 -apply (erule_tac x = "m" in rev_bspec)
     9.8 +apply (erule_tac x = m in rev_bspec)
     9.9  apply (erule nat_induct, simp) 
    9.10  apply (rule ballI)
    9.11  apply (rename_tac i j)
    10.1 --- a/src/ZF/OrderArith.thy	Thu Jan 23 09:16:53 2003 +0100
    10.2 +++ b/src/ZF/OrderArith.thy	Thu Jan 23 10:30:14 2003 +0100
    10.3 @@ -88,12 +88,12 @@
    10.4   prefer 2
    10.5   apply (erule_tac V = "y : A + B" in thin_rl)
    10.6   apply (rule_tac ballI)
    10.7 - apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
    10.8 + apply (erule_tac r = r and a = x in wf_on_induct, assumption)
    10.9   apply blast 
   10.10  txt{*Returning to main part of proof*}
   10.11  apply safe
   10.12  apply blast
   10.13 -apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast) 
   10.14 +apply (erule_tac r = s and a = ya in wf_on_induct, assumption, blast) 
   10.15  done
   10.16  
   10.17  lemma wf_radd: "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
   10.18 @@ -193,9 +193,9 @@
   10.19  apply (erule SigmaE)
   10.20  apply (erule ssubst)
   10.21  apply (subgoal_tac "ALL b:B. <x,b>: Ba", blast)
   10.22 -apply (erule_tac a = "x" in wf_on_induct, assumption)
   10.23 +apply (erule_tac a = x in wf_on_induct, assumption)
   10.24  apply (rule ballI)
   10.25 -apply (erule_tac a = "b" in wf_on_induct, assumption)
   10.26 +apply (erule_tac a = b in wf_on_induct, assumption)
   10.27  apply (best elim!: rmultE bspec [THEN mp])
   10.28  done
   10.29  
   10.30 @@ -236,7 +236,7 @@
   10.31  done
   10.32  
   10.33  lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
   10.34 -by (rule_tac d = "snd" in lam_bijective, auto)
   10.35 +by (rule_tac d = snd in lam_bijective, auto)
   10.36  
   10.37  (*Used??*)
   10.38  lemma singleton_prod_ord_iso:
   10.39 @@ -310,8 +310,7 @@
   10.40  subsubsection{*Type checking*}
   10.41  
   10.42  lemma rvimage_type: "rvimage(A,f,r) <= A*A"
   10.43 -apply (unfold rvimage_def, rule Collect_subset)
   10.44 -done
   10.45 +by (unfold rvimage_def, rule Collect_subset)
   10.46  
   10.47  lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
   10.48  
   10.49 @@ -539,8 +538,7 @@
   10.50  apply (rename_tac u) 
   10.51  apply (drule_tac x=u in bspec, blast) 
   10.52  apply (erule mp, clarify)
   10.53 -apply (frule ok, assumption+); 
   10.54 -apply blast 
   10.55 +apply (frule ok, assumption+, blast) 
   10.56  done
   10.57  
   10.58  
    11.1 --- a/src/ZF/Ordinal.thy	Thu Jan 23 09:16:53 2003 +0100
    11.2 +++ b/src/ZF/Ordinal.thy	Thu Jan 23 10:30:14 2003 +0100
    11.3 @@ -173,7 +173,7 @@
    11.4  (*There is no set of all ordinals, for then it would contain itself*)
    11.5  lemma ON_class: "~ (ALL i. i:X <-> Ord(i))"
    11.6  apply (rule notI)
    11.7 -apply (frule_tac x = "X" in spec)
    11.8 +apply (frule_tac x = X in spec)
    11.9  apply (safe elim!: mem_irrefl)
   11.10  apply (erule swap, rule OrdI [OF _ Ord_is_Transset])
   11.11  apply (simp add: Transset_def)
   11.12 @@ -366,13 +366,13 @@
   11.13  
   11.14  lemma Ord_linear2:
   11.15      "[| Ord(i);  Ord(j);  i<j ==> P;  j le i ==> P |]  ==> P"
   11.16 -apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
   11.17 +apply (rule_tac i = i and j = j in Ord_linear_lt)
   11.18  apply (blast intro: leI le_eqI sym ) +
   11.19  done
   11.20  
   11.21  lemma Ord_linear_le:
   11.22      "[| Ord(i);  Ord(j);  i le j ==> P;  j le i ==> P |]  ==> P"
   11.23 -apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
   11.24 +apply (rule_tac i = i and j = j in Ord_linear_lt)
   11.25  apply (blast intro: leI le_eqI ) +
   11.26  done
   11.27  
   11.28 @@ -380,7 +380,7 @@
   11.29  by (blast elim!: leE elim: lt_asym)
   11.30  
   11.31  lemma not_lt_imp_le: "[| ~ i<j;  Ord(i);  Ord(j) |] ==> j le i"
   11.32 -by (rule_tac i = "i" and j = "j" in Ord_linear2, auto)
   11.33 +by (rule_tac i = i and j = j in Ord_linear2, auto)
   11.34  
   11.35  subsubsection{*Some Rewrite Rules for <, le*}
   11.36  
   11.37 @@ -495,7 +495,7 @@
   11.38  
   11.39  (*Replacing k by succ(k') yields the similar rule for le!*)
   11.40  lemma Un_least_lt: "[| i<k;  j<k |] ==> i Un j < k"
   11.41 -apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
   11.42 +apply (rule_tac i = i and j = j in Ord_linear_le)
   11.43  apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord) 
   11.44  done
   11.45  
   11.46 @@ -513,7 +513,7 @@
   11.47  
   11.48  (*Replacing k by succ(k') yields the similar rule for le!*)
   11.49  lemma Int_greatest_lt: "[| i<k;  j<k |] ==> i Int j < k"
   11.50 -apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
   11.51 +apply (rule_tac i = i and j = j in Ord_linear_le)
   11.52  apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) 
   11.53  done
   11.54  
    12.1 --- a/src/ZF/Perm.thy	Thu Jan 23 09:16:53 2003 +0100
    12.2 +++ b/src/ZF/Perm.thy	Thu Jan 23 10:30:14 2003 +0100
    12.3 @@ -69,7 +69,7 @@
    12.4          !!y. y:B ==> d(y): A;            
    12.5          !!y. y:B ==> c(d(y)) = y         
    12.6       |] ==> (lam x:A. c(x)) : surj(A,B)"
    12.7 -apply (rule_tac d = "d" in f_imp_surjective) 
    12.8 +apply (rule_tac d = d in f_imp_surjective) 
    12.9  apply (simp_all add: lam_type)
   12.10  done
   12.11  
   12.12 @@ -112,7 +112,7 @@
   12.13      "[| !!x. x:A ==> c(x): B;            
   12.14          !!x. x:A ==> d(c(x)) = x |]
   12.15       ==> (lam x:A. c(x)) : inj(A,B)"
   12.16 -apply (rule_tac d = "d" in f_imp_injective)
   12.17 +apply (rule_tac d = d in f_imp_injective)
   12.18  apply (simp_all add: lam_type)
   12.19  done
   12.20  
   12.21 @@ -143,7 +143,7 @@
   12.22  
   12.23  lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y))   
   12.24        ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)"
   12.25 -apply (rule_tac d = "f" in lam_bijective)
   12.26 +apply (rule_tac d = f in lam_bijective)
   12.27  apply (auto simp add: the_equality2)
   12.28  done
   12.29  
   12.30 @@ -387,8 +387,8 @@
   12.31  lemma comp_mem_injD2: 
   12.32      "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
   12.33  apply (unfold inj_def surj_def, safe)
   12.34 -apply (rule_tac x1 = "x" in bspec [THEN bexE])
   12.35 -apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+, safe)
   12.36 +apply (rule_tac x1 = x in bspec [THEN bexE])
   12.37 +apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe)
   12.38  apply (rule_tac t = "op ` (g) " in subst_context)
   12.39  apply (erule asm_rl bspec [THEN bspec, THEN mp])+
   12.40  apply (simp (no_asm_simp))
    13.1 --- a/src/ZF/QPair.thy	Thu Jan 23 09:16:53 2003 +0100
    13.2 +++ b/src/ZF/QPair.thy	Thu Jan 23 10:30:14 2003 +0100
    13.3 @@ -283,7 +283,7 @@
    13.4          !!x. x: A ==> c(x): C(QInl(x));    
    13.5          !!y. y: B ==> d(y): C(QInr(y))  
    13.6       |] ==> qcase(c,d,u) : C(u)"
    13.7 -by (simp add: qsum_defs , auto) 
    13.8 +by (simp add: qsum_defs, auto) 
    13.9  
   13.10  (** Rules for the Part primitive **)
   13.11  
    14.1 --- a/src/ZF/Trancl.thy	Thu Jan 23 09:16:53 2003 +0100
    14.2 +++ b/src/ZF/Trancl.thy	Thu Jan 23 10:30:14 2003 +0100
    14.3 @@ -166,7 +166,7 @@
    14.4  lemma trans_rtrancl: "trans(r^*)"
    14.5  apply (unfold trans_def)
    14.6  apply (intro allI impI)
    14.7 -apply (erule_tac b = "z" in rtrancl_induct, assumption)
    14.8 +apply (erule_tac b = z in rtrancl_induct, assumption)
    14.9  apply (blast intro: rtrancl_into_rtrancl) 
   14.10  done
   14.11  
    15.1 --- a/src/ZF/Univ.thy	Thu Jan 23 09:16:53 2003 +0100
    15.2 +++ b/src/ZF/Univ.thy	Thu Jan 23 10:30:14 2003 +0100
    15.3 @@ -147,7 +147,7 @@
    15.4  
    15.5  lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
    15.6  apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
    15.7 -apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst])
    15.8 +apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst])
    15.9  apply (subst rank_succ)
   15.10  apply (rule Ord_rank [THEN Vfrom_succ_lemma])
   15.11  done
    16.1 --- a/src/ZF/WF.thy	Thu Jan 23 09:16:53 2003 +0100
    16.2 +++ b/src/ZF/WF.thy	Thu Jan 23 10:30:14 2003 +0100
    16.3 @@ -79,7 +79,7 @@
    16.4   shows         "wf[A](r)"
    16.5  apply (unfold wf_on_def wf_def)
    16.6  apply (rule equals0I [THEN disjCI, THEN allI])
    16.7 -apply (rule_tac Z = "Z" in prem, blast+)
    16.8 +apply (rule_tac Z = Z in prem, blast+)
    16.9  done
   16.10  
   16.11  text{*If @{term r} allows well-founded induction over @{term A}
   16.12 @@ -192,7 +192,7 @@
   16.13      "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
   16.14  apply (rule wf_onI2)
   16.15  apply (frule bspec [THEN mp], assumption+)
   16.16 -apply (erule_tac a = "y" in wf_on_induct, assumption)
   16.17 +apply (erule_tac a = y in wf_on_induct, assumption)
   16.18  apply (blast elim: tranclE, blast) 
   16.19  done
   16.20  
   16.21 @@ -232,8 +232,8 @@
   16.22  lemma is_recfun_equal [rule_format]:
   16.23       "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]
   16.24        ==> <x,a>:r --> <x,b>:r --> f`x=g`x"
   16.25 -apply (frule_tac f = "f" in is_recfun_type)
   16.26 -apply (frule_tac f = "g" in is_recfun_type)
   16.27 +apply (frule_tac f = f in is_recfun_type)
   16.28 +apply (frule_tac f = g in is_recfun_type)
   16.29  apply (simp add: is_recfun_def)
   16.30  apply (erule_tac a=x in wf_induct)
   16.31  apply (intro impI)
   16.32 @@ -250,7 +250,7 @@
   16.33       "[| wf(r);  trans(r);
   16.34           is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]
   16.35        ==> restrict(f, r-``{b}) = g"
   16.36 -apply (frule_tac f = "f" in is_recfun_type)
   16.37 +apply (frule_tac f = f in is_recfun_type)
   16.38  apply (rule fun_extension)
   16.39    apply (blast dest: transD intro: restrict_type2)
   16.40   apply (erule is_recfun_type, simp)
   16.41 @@ -294,7 +294,7 @@
   16.42   apply (blast dest: transD)
   16.43  apply (frule spec [THEN mp], assumption)
   16.44  apply (subgoal_tac "<xa,a1> : r")
   16.45 - apply (drule_tac x1 = "xa" in spec [THEN mp], assumption)
   16.46 + apply (drule_tac x1 = xa in spec [THEN mp], assumption)
   16.47  apply (simp add: vimage_singleton_iff 
   16.48                   apply_recfun is_recfun_cut)
   16.49  apply (blast dest: transD)
   16.50 @@ -343,7 +343,7 @@
   16.51      "[| wf(r);  a:A;  field(r)<=A;
   16.52          !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)
   16.53       |] ==> wfrec(r,a,H) : B(a)"
   16.54 -apply (rule_tac a = "a" in wf_induct2, assumption+)
   16.55 +apply (rule_tac a = a in wf_induct2, assumption+)
   16.56  apply (subst wfrec, assumption)
   16.57  apply (simp add: lam_type underD)  
   16.58  done
    17.1 --- a/src/ZF/Zorn.thy	Thu Jan 23 09:16:53 2003 +0100
    17.2 +++ b/src/ZF/Zorn.thy	Thu Jan 23 10:30:14 2003 +0100
    17.3 @@ -115,7 +115,7 @@
    17.4  apply (erule TFin_induct)
    17.5  apply (rule impI [THEN ballI])
    17.6  txt{*case split using @{text TFin_linear_lemma1}*}
    17.7 -apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
    17.8 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
    17.9         assumption+)
   17.10  apply (blast del: subsetI
   17.11  	     intro: increasing_trans subsetI, blast)
   17.12 @@ -127,7 +127,7 @@
   17.13  apply (rule ballI)
   17.14  apply (drule bspec, assumption)
   17.15  apply (drule subsetD, assumption)
   17.16 -apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
   17.17 +apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
   17.18         assumption+, blast)
   17.19  apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
   17.20  apply (blast dest: TFin_is_subset)+
   17.21 @@ -156,8 +156,7 @@
   17.22       "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n <= m"
   17.23  apply (erule TFin_induct)
   17.24  apply (drule TFin_subsetD)
   17.25 -apply (assumption+, force)
   17.26 -apply blast
   17.27 +apply (assumption+, force, blast)
   17.28  done
   17.29  
   17.30  text{*Property 3.3 of section 3.3*}
   17.31 @@ -208,8 +207,7 @@
   17.32       "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
   17.33        ==> ch ` super(S,X) \<noteq> X"
   17.34  apply (rule notI)
   17.35 -apply (drule choice_super, assumption)
   17.36 -apply assumption
   17.37 +apply (drule choice_super, assumption, assumption)
   17.38  apply (simp add: super_def)
   17.39  done
   17.40