# HG changeset patch
# User paulson
# Date 1043314214 -3600
# Node ID b9f6154427a4ade03b01bc35a19e1331ca5f5ddc
# Parent  3294f727e20d48a9dfada5f6f3e7d97065bf4b0e
tidying (by script)

diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Arith.thy
--- a/src/ZF/Arith.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Arith.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -200,7 +200,7 @@
 (*Must simplify BEFORE the induction: else we get a critical pair*)
 lemma diff_succ_succ [simp]: "succ(m) #- succ(n) = m #- n"
 apply (simp add: natify_succ diff_def)
-apply (rule_tac x1 = "n" in natify_in_nat [THEN nat_induct], auto)
+apply (rule_tac x1 = n in natify_in_nat [THEN nat_induct], auto)
 done
 
 (*This defining property is no longer wanted*)
@@ -212,7 +212,7 @@
 
 lemma diff_le_self: "m:nat ==> (m #- n) le m"
 apply (subgoal_tac " (m #- natify (n)) le m")
-apply (rule_tac [2] m = "m" and n = "natify (n) " in diff_induct)
+apply (rule_tac [2] m = m and n = "natify (n) " in diff_induct)
 apply (erule_tac [6] leE)
 apply (simp_all add: le_iff)
 done
@@ -528,7 +528,7 @@
 
 lemma less_diff_conv [rule_format]:
      "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)"
-by (erule_tac m = "k" in diff_induct, auto)
+by (erule_tac m = k in diff_induct, auto)
 
 lemmas nat_typechecks = rec_type nat_0I nat_1I nat_succI Ord_nat
 
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/ArithSimp.thy
--- a/src/ZF/ArithSimp.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/ArithSimp.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -24,7 +24,7 @@
 lemma add_diff_inverse: "[| n le m;  m:nat |] ==> n #+ (m#-n) = m"
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (erule rev_mp)
-apply (rule_tac m = "m" and n = "n" in diff_induct, auto)
+apply (rule_tac m = m and n = n in diff_induct, auto)
 done
 
 lemma add_diff_inverse2: "[| n le m;  m:nat |] ==> (m#-n) #+ n = m"
@@ -36,13 +36,13 @@
 lemma diff_succ: "[| n le m;  m:nat |] ==> succ(m) #- n = succ(m#-n)"
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (erule rev_mp)
-apply (rule_tac m = "m" and n = "n" in diff_induct)
+apply (rule_tac m = m and n = n in diff_induct)
 apply (simp_all (no_asm_simp))
 done
 
 lemma zero_less_diff [simp]:
      "[| m: nat; n: nat |] ==> 0 < (n #- m)   <->   m<n"
-apply (rule_tac m = "m" and n = "n" in diff_induct)
+apply (rule_tac m = m and n = n in diff_induct)
 apply (simp_all (no_asm_simp))
 done
 
@@ -67,7 +67,7 @@
 apply (frule lt_nat_in_nat, erule nat_succI)
 apply (erule rev_mp)
 apply (erule rev_mp)
-apply (rule_tac m = "m" and n = "n" in diff_induct)
+apply (rule_tac m = m and n = n in diff_induct)
 apply (simp_all (no_asm_simp) add: diff_le_self)
 done
 
@@ -236,7 +236,7 @@
 done
 
 lemma mod_1_eq [simp]: "m mod 1 = 0"
-by (cut_tac n = "1" in mod_less_divisor, auto)
+by (cut_tac n = 1 in mod_less_divisor, auto)
 
 lemma mod2_cases: "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)"
 apply (subgoal_tac "k mod 2: 2")
@@ -257,7 +257,7 @@
 done
 
 lemma mod2_add_self [simp]: "(m#+m) mod 2 = 0"
-by (cut_tac n = "0" in mod2_add_more, auto)
+by (cut_tac n = 0 in mod2_add_more, auto)
 
 
 subsection{*Additional theorems about @{text "\<le>"}*}
@@ -368,7 +368,7 @@
 done
 
 lemma mult_le_cancel_le1: "k : nat ==> k #* m le k \<longleftrightarrow> (0 < k \<longrightarrow> natify(m) le 1)"
-by (cut_tac k = "k" and m = "m" and n = "1" in mult_le_cancel1, auto)
+by (cut_tac k = k and m = m and n = 1 in mult_le_cancel1, auto)
 
 lemma Ord_eq_iff_le: "[| Ord(m); Ord(n) |] ==> m=n <-> (m le n & n le m)"
 by (blast intro: le_anti_sym)
@@ -395,7 +395,7 @@
 
 lemma div_cancel_raw:
      "[| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n"
-apply (erule_tac i = "m" in complete_induct)
+apply (erule_tac i = m in complete_induct)
 apply (case_tac "x<n")
  apply (simp add: div_less zero_lt_mult_iff mult_lt_mono2)
 apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono]
@@ -419,7 +419,7 @@
 apply (case_tac "n=0")
  apply (simp add: DIVISION_BY_ZERO_MOD)
 apply (simp add: nat_into_Ord [THEN Ord_0_lt_iff])
-apply (erule_tac i = "m" in complete_induct)
+apply (erule_tac i = m in complete_induct)
 apply (case_tac "x<n")
  apply (simp (no_asm_simp) add: mod_less zero_lt_mult_iff mult_lt_mono2)
 apply (simp add: not_lt_iff_le zero_lt_mult_iff le_refl [THEN mult_le_mono] 
@@ -499,7 +499,7 @@
 
 lemma diff_is_0_lemma:
      "[| m: nat; n: nat |] ==> m #- n = 0 <-> m le n"
-apply (rule_tac m = "m" and n = "n" in diff_induct, simp_all)
+apply (rule_tac m = m and n = n in diff_induct, simp_all)
 done
 
 lemma diff_is_0_iff: "m #- n = 0 <-> natify(m) le natify(n)"
@@ -514,8 +514,7 @@
       (P(a #- b)) <-> ((a < b -->P(0)) & (ALL d:nat. a = b #+ d --> P(d)))"
 apply (case_tac "a < b")
  apply (force simp add: nat_lt_imp_diff_eq_0)
-apply (rule iffI, force) 
-apply simp 
+apply (rule iffI, force, simp) 
 apply (drule_tac x="a#-b" in bspec)
 apply (simp_all add: Ordinal.not_lt_iff_le add_diff_inverse) 
 done
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Cardinal.thy
--- a/src/ZF/Cardinal.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Cardinal.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -495,7 +495,7 @@
 apply (induct_tac m)
 apply (blast intro!: nat_0_le)
 apply (rule ballI)
-apply (erule_tac n = "n" in natE)
+apply (erule_tac n = n in natE)
 apply (simp (no_asm_simp) add: lepoll_def inj_def)
 apply (blast intro!: succ_leI dest!: succ_lepoll_succD)
 done
@@ -859,7 +859,7 @@
 apply (rule Diff_sing_eqpoll [THEN revcut_rl])
 prefer 2 apply assumption
 apply assumption
-apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
+apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
 apply (rule Fin.consI, blast)
 apply (blast intro: subset_consI [THEN Fin_mono, THEN subsetD])
 (*Now for the lemma assumed above*)
@@ -907,7 +907,7 @@
 apply (subgoal_tac [2] "A-{a}=A", auto)
 apply (rule_tac x = "succ (n) " in bexI)
 apply (subgoal_tac "cons (a, A - {a}) = A & cons (n, n) = succ (n) ")
-apply (drule_tac a = "a" and b = "n" in cons_eqpoll_cong)
+apply (drule_tac a = a and b = n in cons_eqpoll_cong)
 apply (auto dest: mem_irrefl)
 done
 
@@ -976,7 +976,7 @@
  apply (drule_tac x = x in bspec, assumption)
  apply (blast elim: mem_irrefl mem_asym)
 txt{*other case*} 
-apply (drule_tac x = "Z" in spec, blast) 
+apply (drule_tac x = Z in spec, blast) 
 done
 
 lemma nat_well_ord_converse_Memrel: "n:nat ==> well_ord(n,converse(Memrel(n)))"
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/CardinalArith.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -585,14 +585,14 @@
 (*??WHAT A MESS!*)  
 apply (rule InfCard_is_Limit [THEN ordermap_csquare_le, THEN lt_trans1],
        (assumption | rule refl | erule ltI)+) 
-apply (rule_tac i = "xa Un ya" and j = "nat" in Ord_linear2,
+apply (rule_tac i = "xa Un ya" and j = nat in Ord_linear2,
        simp_all add: Ord_Un Ord_nat)
 prefer 2 (*case nat le (xa Un ya) *)
  apply (simp add: le_imp_subset [THEN nat_succ_eqpoll, THEN cardinal_cong] 
                   le_succ_iff InfCard_def Card_cardinal Un_least_lt Ord_Un
                 ltI nat_le_cardinal Ord_cardinal_le [THEN lt_trans1, THEN ltD])
 (*the finite case: xa Un ya < nat *)
-apply (rule_tac j = "nat" in lt_trans2)
+apply (rule_tac j = nat in lt_trans2)
  apply (simp add: lt_def nat_cmult_eq_mult nat_succI mult_type
                   nat_into_Card [THEN Card_cardinal_eq]  Ord_nat)
 apply (simp add: InfCard_def)
@@ -645,7 +645,7 @@
 
 (*Corollary 10.13 (1), for cardinal multiplication*)
 lemma InfCard_cmult_eq: "[| InfCard(K);  InfCard(L) |] ==> K |*| L = K Un L"
-apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
+apply (rule_tac i = K and j = L in Ord_linear_le)
 apply (typecheck add: InfCard_is_Card Card_is_Ord)
 apply (rule cmult_commute [THEN ssubst])
 apply (rule Un_commute [THEN ssubst])
@@ -669,7 +669,7 @@
 done
 
 lemma InfCard_cadd_eq: "[| InfCard(K);  InfCard(L) |] ==> K |+| L = K Un L"
-apply (rule_tac i = "K" and j = "L" in Ord_linear_le)
+apply (rule_tac i = K and j = L in Ord_linear_le)
 apply (typecheck add: InfCard_is_Card Card_is_Ord)
 apply (rule cadd_commute [THEN ssubst])
 apply (rule Un_commute [THEN ssubst])
@@ -812,7 +812,7 @@
 
 lemma Finite_imp_succ_cardinal_Diff:
      "[| Finite(A);  a:A |] ==> succ(|A-{a}|) = |A|"
-apply (rule_tac b = "A" in cons_Diff [THEN subst], assumption)
+apply (rule_tac b = A in cons_Diff [THEN subst], assumption)
 apply (simp add: Finite_imp_cardinal_cons Diff_subset [THEN subset_Finite])
 apply (simp add: cons_Diff)
 done
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Cardinal_AC.thy
--- a/src/ZF/Cardinal_AC.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Cardinal_AC.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -83,7 +83,7 @@
 lemma surj_implies_inj: "f: surj(X,Y) ==> EX g. g: inj(Y,X)"
 apply (unfold surj_def)
 apply (erule CollectE)
-apply (rule_tac A1 = "Y" and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
+apply (rule_tac A1 = Y and B1 = "%y. f-``{y}" in AC_Pi [THEN exE])
 apply (fast elim!: apply_Pair)
 apply (blast dest: apply_type Pi_memberD 
              intro: apply_equality Pi_type f_imp_injective)
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Epsilon.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -180,7 +180,7 @@
 lemma transrec_type:
     "[| !!x u. [| x:eclose({a});  u: Pi(x,B) |] ==> H(x,u) : B(x) |]
      ==> transrec(a,H) : B(a)"
-apply (rule_tac i = "a" in arg_in_eclose_sing [THEN eclose_induct])
+apply (rule_tac i = a in arg_in_eclose_sing [THEN eclose_induct])
 apply (subst transrec)
 apply (simp add: lam_type) 
 done
@@ -220,7 +220,7 @@
 by (subst rank_def [THEN def_transrec], simp)
 
 lemma Ord_rank [simp]: "Ord(rank(a))"
-apply (rule_tac a="a" in eps_induct) 
+apply (rule_tac a=a in eps_induct) 
 apply (subst rank)
 apply (rule Ord_succ [THEN Ord_UN])
 apply (erule bspec, assumption)
@@ -233,7 +233,7 @@
 done
 
 lemma rank_lt: "a:b ==> rank(a) < rank(b)"
-apply (rule_tac a1 = "b" in rank [THEN ssubst])
+apply (rule_tac a1 = b in rank [THEN ssubst])
 apply (erule UN_I [THEN ltI])
 apply (rule_tac [2] Ord_UN, auto)
 done
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Finite.thy
--- a/src/ZF/Finite.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Finite.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -90,7 +90,7 @@
 apply (erule Fin_induct)
 apply (simp add: subset_empty_iff)
 apply (simp add: subset_cons_iff distrib_simps, safe)
-apply (erule_tac b = "z" in cons_Diff [THEN subst], simp)
+apply (erule_tac b = z in cons_Diff [THEN subst], simp)
 done
 
 lemma Fin_subset: "[| c<=b;  b: Fin(A) |] ==> c: Fin(A)"
@@ -158,7 +158,7 @@
 apply (erule FiniteFun.induct)
 apply (simp add: subset_empty_iff FiniteFun.intros)
 apply (simp add: subset_cons_iff distrib_simps, safe)
-apply (erule_tac b = "z" in cons_Diff [THEN subst])
+apply (erule_tac b = z in cons_Diff [THEN subst])
 apply (drule spec [THEN mp], assumption)
 apply (fast intro!: FiniteFun.intros)
 done
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/List.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -354,8 +354,7 @@
 
 lemma drop_length [rule_format]:
      "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
-apply (erule list.induct, simp_all)
-apply safe
+apply (erule list.induct, simp_all, safe)
 apply (erule drop_length_Cons)
 apply (rule natE)
 apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
@@ -1121,8 +1120,7 @@
 lemma nth_map_upt [rule_format]:
      "[| m:nat; n:nat |] ==>
       \<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
-apply (rule_tac n = m and m = n in diff_induct, typecheck, simp) 
-apply simp 
+apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp) 
 apply (subst map_succ_upt [symmetric], simp_all, clarify) 
 apply (subgoal_tac "i < length (upt (0, x))")
  prefer 2 
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Nat.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -174,7 +174,7 @@
         !!y. y: nat ==> P(0,succ(y));   
         !!x y. [| x: nat;  y: nat;  P(x,y) |] ==> P(succ(x),succ(y)) |]
      ==> P(m,n)"
-apply (erule_tac x = "m" in rev_bspec)
+apply (erule_tac x = m in rev_bspec)
 apply (erule nat_induct, simp) 
 apply (rule ballI)
 apply (rename_tac i j)
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/OrderArith.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -88,12 +88,12 @@
  prefer 2
  apply (erule_tac V = "y : A + B" in thin_rl)
  apply (rule_tac ballI)
- apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
+ apply (erule_tac r = r and a = x in wf_on_induct, assumption)
  apply blast 
 txt{*Returning to main part of proof*}
 apply safe
 apply blast
-apply (erule_tac r = "s" and a = "ya" in wf_on_induct, assumption, blast) 
+apply (erule_tac r = s and a = ya in wf_on_induct, assumption, blast) 
 done
 
 lemma wf_radd: "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
@@ -193,9 +193,9 @@
 apply (erule SigmaE)
 apply (erule ssubst)
 apply (subgoal_tac "ALL b:B. <x,b>: Ba", blast)
-apply (erule_tac a = "x" in wf_on_induct, assumption)
+apply (erule_tac a = x in wf_on_induct, assumption)
 apply (rule ballI)
-apply (erule_tac a = "b" in wf_on_induct, assumption)
+apply (erule_tac a = b in wf_on_induct, assumption)
 apply (best elim!: rmultE bspec [THEN mp])
 done
 
@@ -236,7 +236,7 @@
 done
 
 lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
-by (rule_tac d = "snd" in lam_bijective, auto)
+by (rule_tac d = snd in lam_bijective, auto)
 
 (*Used??*)
 lemma singleton_prod_ord_iso:
@@ -310,8 +310,7 @@
 subsubsection{*Type checking*}
 
 lemma rvimage_type: "rvimage(A,f,r) <= A*A"
-apply (unfold rvimage_def, rule Collect_subset)
-done
+by (unfold rvimage_def, rule Collect_subset)
 
 lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
 
@@ -539,8 +538,7 @@
 apply (rename_tac u) 
 apply (drule_tac x=u in bspec, blast) 
 apply (erule mp, clarify)
-apply (frule ok, assumption+); 
-apply blast 
+apply (frule ok, assumption+, blast) 
 done
 
 
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Ordinal.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -173,7 +173,7 @@
 (*There is no set of all ordinals, for then it would contain itself*)
 lemma ON_class: "~ (ALL i. i:X <-> Ord(i))"
 apply (rule notI)
-apply (frule_tac x = "X" in spec)
+apply (frule_tac x = X in spec)
 apply (safe elim!: mem_irrefl)
 apply (erule swap, rule OrdI [OF _ Ord_is_Transset])
 apply (simp add: Transset_def)
@@ -366,13 +366,13 @@
 
 lemma Ord_linear2:
     "[| Ord(i);  Ord(j);  i<j ==> P;  j le i ==> P |]  ==> P"
-apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
+apply (rule_tac i = i and j = j in Ord_linear_lt)
 apply (blast intro: leI le_eqI sym ) +
 done
 
 lemma Ord_linear_le:
     "[| Ord(i);  Ord(j);  i le j ==> P;  j le i ==> P |]  ==> P"
-apply (rule_tac i = "i" and j = "j" in Ord_linear_lt)
+apply (rule_tac i = i and j = j in Ord_linear_lt)
 apply (blast intro: leI le_eqI ) +
 done
 
@@ -380,7 +380,7 @@
 by (blast elim!: leE elim: lt_asym)
 
 lemma not_lt_imp_le: "[| ~ i<j;  Ord(i);  Ord(j) |] ==> j le i"
-by (rule_tac i = "i" and j = "j" in Ord_linear2, auto)
+by (rule_tac i = i and j = j in Ord_linear2, auto)
 
 subsubsection{*Some Rewrite Rules for <, le*}
 
@@ -495,7 +495,7 @@
 
 (*Replacing k by succ(k') yields the similar rule for le!*)
 lemma Un_least_lt: "[| i<k;  j<k |] ==> i Un j < k"
-apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
+apply (rule_tac i = i and j = j in Ord_linear_le)
 apply (auto simp add: Un_commute le_subset_iff subset_Un_iff lt_Ord) 
 done
 
@@ -513,7 +513,7 @@
 
 (*Replacing k by succ(k') yields the similar rule for le!*)
 lemma Int_greatest_lt: "[| i<k;  j<k |] ==> i Int j < k"
-apply (rule_tac i = "i" and j = "j" in Ord_linear_le)
+apply (rule_tac i = i and j = j in Ord_linear_le)
 apply (auto simp add: Int_commute le_subset_iff subset_Int_iff lt_Ord) 
 done
 
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Perm.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -69,7 +69,7 @@
         !!y. y:B ==> d(y): A;            
         !!y. y:B ==> c(d(y)) = y         
      |] ==> (lam x:A. c(x)) : surj(A,B)"
-apply (rule_tac d = "d" in f_imp_surjective) 
+apply (rule_tac d = d in f_imp_surjective) 
 apply (simp_all add: lam_type)
 done
 
@@ -112,7 +112,7 @@
     "[| !!x. x:A ==> c(x): B;            
         !!x. x:A ==> d(c(x)) = x |]
      ==> (lam x:A. c(x)) : inj(A,B)"
-apply (rule_tac d = "d" in f_imp_injective)
+apply (rule_tac d = d in f_imp_injective)
 apply (simp_all add: lam_type)
 done
 
@@ -143,7 +143,7 @@
 
 lemma RepFun_bijective: "(ALL y : x. EX! y'. f(y') = f(y))   
       ==> (lam z:{f(y). y:x}. THE y. f(y) = z) : bij({f(y). y:x}, x)"
-apply (rule_tac d = "f" in lam_bijective)
+apply (rule_tac d = f in lam_bijective)
 apply (auto simp add: the_equality2)
 done
 
@@ -387,8 +387,8 @@
 lemma comp_mem_injD2: 
     "[| (f O g): inj(A,C);  g: surj(A,B);  f: B->C |] ==> f: inj(B,C)"
 apply (unfold inj_def surj_def, safe)
-apply (rule_tac x1 = "x" in bspec [THEN bexE])
-apply (erule_tac [3] x1 = "w" in bspec [THEN bexE], assumption+, safe)
+apply (rule_tac x1 = x in bspec [THEN bexE])
+apply (erule_tac [3] x1 = w in bspec [THEN bexE], assumption+, safe)
 apply (rule_tac t = "op ` (g) " in subst_context)
 apply (erule asm_rl bspec [THEN bspec, THEN mp])+
 apply (simp (no_asm_simp))
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/QPair.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -283,7 +283,7 @@
         !!x. x: A ==> c(x): C(QInl(x));    
         !!y. y: B ==> d(y): C(QInr(y))  
      |] ==> qcase(c,d,u) : C(u)"
-by (simp add: qsum_defs , auto) 
+by (simp add: qsum_defs, auto) 
 
 (** Rules for the Part primitive **)
 
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Trancl.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -166,7 +166,7 @@
 lemma trans_rtrancl: "trans(r^*)"
 apply (unfold trans_def)
 apply (intro allI impI)
-apply (erule_tac b = "z" in rtrancl_induct, assumption)
+apply (erule_tac b = z in rtrancl_induct, assumption)
 apply (blast intro: rtrancl_into_rtrancl) 
 done
 
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Univ.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -147,7 +147,7 @@
 
 lemma Vfrom_succ: "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))"
 apply (rule_tac x1 = "succ (i)" in Vfrom_rank_eq [THEN subst])
-apply (rule_tac x1 = "i" in Vfrom_rank_eq [THEN subst])
+apply (rule_tac x1 = i in Vfrom_rank_eq [THEN subst])
 apply (subst rank_succ)
 apply (rule Ord_rank [THEN Vfrom_succ_lemma])
 done
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/WF.thy
--- a/src/ZF/WF.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/WF.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -79,7 +79,7 @@
  shows         "wf[A](r)"
 apply (unfold wf_on_def wf_def)
 apply (rule equals0I [THEN disjCI, THEN allI])
-apply (rule_tac Z = "Z" in prem, blast+)
+apply (rule_tac Z = Z in prem, blast+)
 done
 
 text{*If @{term r} allows well-founded induction over @{term A}
@@ -192,7 +192,7 @@
     "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
 apply (rule wf_onI2)
 apply (frule bspec [THEN mp], assumption+)
-apply (erule_tac a = "y" in wf_on_induct, assumption)
+apply (erule_tac a = y in wf_on_induct, assumption)
 apply (blast elim: tranclE, blast) 
 done
 
@@ -232,8 +232,8 @@
 lemma is_recfun_equal [rule_format]:
      "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]
       ==> <x,a>:r --> <x,b>:r --> f`x=g`x"
-apply (frule_tac f = "f" in is_recfun_type)
-apply (frule_tac f = "g" in is_recfun_type)
+apply (frule_tac f = f in is_recfun_type)
+apply (frule_tac f = g in is_recfun_type)
 apply (simp add: is_recfun_def)
 apply (erule_tac a=x in wf_induct)
 apply (intro impI)
@@ -250,7 +250,7 @@
      "[| wf(r);  trans(r);
          is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]
       ==> restrict(f, r-``{b}) = g"
-apply (frule_tac f = "f" in is_recfun_type)
+apply (frule_tac f = f in is_recfun_type)
 apply (rule fun_extension)
   apply (blast dest: transD intro: restrict_type2)
  apply (erule is_recfun_type, simp)
@@ -294,7 +294,7 @@
  apply (blast dest: transD)
 apply (frule spec [THEN mp], assumption)
 apply (subgoal_tac "<xa,a1> : r")
- apply (drule_tac x1 = "xa" in spec [THEN mp], assumption)
+ apply (drule_tac x1 = xa in spec [THEN mp], assumption)
 apply (simp add: vimage_singleton_iff 
                  apply_recfun is_recfun_cut)
 apply (blast dest: transD)
@@ -343,7 +343,7 @@
     "[| wf(r);  a:A;  field(r)<=A;
         !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)
      |] ==> wfrec(r,a,H) : B(a)"
-apply (rule_tac a = "a" in wf_induct2, assumption+)
+apply (rule_tac a = a in wf_induct2, assumption+)
 apply (subst wfrec, assumption)
 apply (simp add: lam_type underD)  
 done
diff -r 3294f727e20d -r b9f6154427a4 src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Thu Jan 23 09:16:53 2003 +0100
+++ b/src/ZF/Zorn.thy	Thu Jan 23 10:30:14 2003 +0100
@@ -115,7 +115,7 @@
 apply (erule TFin_induct)
 apply (rule impI [THEN ballI])
 txt{*case split using @{text TFin_linear_lemma1}*}
-apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
+apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
        assumption+)
 apply (blast del: subsetI
 	     intro: increasing_trans subsetI, blast)
@@ -127,7 +127,7 @@
 apply (rule ballI)
 apply (drule bspec, assumption)
 apply (drule subsetD, assumption)
-apply (rule_tac n1 = "n" and m1 = "x" in TFin_linear_lemma1 [THEN disjE],
+apply (rule_tac n1 = n and m1 = x in TFin_linear_lemma1 [THEN disjE],
        assumption+, blast)
 apply (erule increasingD2 [THEN subset_trans, THEN disjI1])
 apply (blast dest: TFin_is_subset)+
@@ -156,8 +156,7 @@
      "[| n \<in> TFin(S,next);  m \<in> TFin(S,next);  m = next`m |] ==> n <= m"
 apply (erule TFin_induct)
 apply (drule TFin_subsetD)
-apply (assumption+, force)
-apply blast
+apply (assumption+, force, blast)
 done
 
 text{*Property 3.3 of section 3.3*}
@@ -208,8 +207,7 @@
      "[| ch \<in> (\<Pi>X \<in> Pow(chain(S)) - {0}. X); X \<in> chain(S);  X \<notin> maxchain(S) |]
       ==> ch ` super(S,X) \<noteq> X"
 apply (rule notI)
-apply (drule choice_super, assumption)
-apply assumption
+apply (drule choice_super, assumption, assumption)
 apply (simp add: super_def)
 done