Proofs needed to be updated because induction now preserves name of
authornipkow
Mon Oct 11 07:42:22 2004 +0200 (2004-10-11)
changeset 15236f289e8ba2bb3
parent 15235 614a804d7116
child 15237 250e9be7a09d
Proofs needed to be updated because induction now preserves name of
induction variable.
src/HOL/Auth/Guard/Extensions.thy
src/HOL/Auth/Guard/Guard.thy
src/HOL/Auth/Guard/GuardK.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/HoareParallel/RG_Tran.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Lambda/Type.thy
src/HOL/Lambda/WeakNorm.thy
src/HOL/List.thy
src/HOL/Matrix/Float.thy
src/HOL/Matrix/MatrixGeneral.thy
src/HOL/Matrix/SparseMatrix.thy
src/HOL/MicroJava/Comp/CorrComp.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/NumberTheory/Chinese.thy
src/HOL/NumberTheory/Factorization.thy
src/HOL/NumberTheory/WilsonRuss.thy
src/HOL/UNITY/Transformers.thy
src/HOL/W0/W0.thy
     1.1 --- a/src/HOL/Auth/Guard/Extensions.thy	Mon Oct 11 07:39:19 2004 +0200
     1.2 +++ b/src/HOL/Auth/Guard/Extensions.thy	Mon Oct 11 07:42:22 2004 +0200
     1.3 @@ -589,11 +589,11 @@
     1.4  apply (case_tac "A=Spy", blast dest: parts_knows_Spy_subset_used)
     1.5  apply (induct evs)
     1.6  apply (simp add: used.simps, blast)
     1.7 -apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify)
     1.8 +apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
     1.9  apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
    1.10  apply (erule initState_used)
    1.11  apply (case_tac a, auto)
    1.12 -apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says)
    1.13 +apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
    1.14  by (auto dest: Says_imp_used intro: used_ConsI)
    1.15  
    1.16  lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
    1.17 @@ -602,10 +602,10 @@
    1.18  apply (simp, blast dest: parts_knows_Spy_subset_used)
    1.19  apply (induct evs)
    1.20  apply (simp add: knows_max_def used.simps, blast)
    1.21 -apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify)
    1.22 +apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
    1.23  apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
    1.24  apply (case_tac a, auto)
    1.25 -apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says)
    1.26 +apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
    1.27  by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI)
    1.28  
    1.29  lemma not_used_not_known: "[| evs:p; X ~:used evs;
     2.1 --- a/src/HOL/Auth/Guard/Guard.thy	Mon Oct 11 07:39:19 2004 +0200
     2.2 +++ b/src/HOL/Auth/Guard/Guard.thy	Mon Oct 11 07:42:22 2004 +0200
     2.3 @@ -210,7 +210,7 @@
     2.4  
     2.5  lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
     2.6  apply (induct l, auto)
     2.7 -by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp)
     2.8 +by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
     2.9  
    2.10  lemma parts_cnb: "Z:parts (set l) ==>
    2.11  cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
    2.12 @@ -227,15 +227,15 @@
    2.13  apply (rule_tac x="[Number nat]" in exI, simp)
    2.14  apply (rule_tac x="[Nonce nat]" in exI, simp)
    2.15  apply (rule_tac x="[Key nat]" in exI, simp)
    2.16 -apply (rule_tac x="[Hash msg]" in exI, simp)
    2.17 +apply (rule_tac x="[Hash X]" in exI, simp)
    2.18  apply (clarify, rule_tac x="l@la" in exI, simp)
    2.19 -by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp)
    2.20 +by (clarify, rule_tac x="[Crypt nat X]" in exI, simp)
    2.21  
    2.22  lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
    2.23  apply (induct l)
    2.24  apply (rule_tac x="[]" in exI, simp, clarsimp)
    2.25 -apply (subgoal_tac "EX l.  kparts {a} = set l & cnb l = crypt_nb a", clarify)
    2.26 -apply (rule_tac x="l@l'" in exI, simp)
    2.27 +apply (subgoal_tac "EX l''.  kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
    2.28 +apply (rule_tac x="l''@l'" in exI, simp)
    2.29  apply (rule kparts_insert_substI, simp)
    2.30  by (rule kparts_msg_set)
    2.31  
     3.1 --- a/src/HOL/Auth/Guard/GuardK.thy	Mon Oct 11 07:39:19 2004 +0200
     3.2 +++ b/src/HOL/Auth/Guard/GuardK.thy	Mon Oct 11 07:42:22 2004 +0200
     3.3 @@ -206,7 +206,7 @@
     3.4  
     3.5  lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
     3.6  apply (induct l, auto)
     3.7 -by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp)
     3.8 +by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
     3.9  
    3.10  lemma parts_cnb: "Z:parts (set l) ==>
    3.11  cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
    3.12 @@ -223,15 +223,15 @@
    3.13  apply (rule_tac x="[Number nat]" in exI, simp)
    3.14  apply (rule_tac x="[Nonce nat]" in exI, simp)
    3.15  apply (rule_tac x="[Key nat]" in exI, simp)
    3.16 -apply (rule_tac x="[Hash msg]" in exI, simp)
    3.17 +apply (rule_tac x="[Hash X]" in exI, simp)
    3.18  apply (clarify, rule_tac x="l@la" in exI, simp)
    3.19 -by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp)
    3.20 +by (clarify, rule_tac x="[Crypt nat X]" in exI, simp)
    3.21  
    3.22  lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
    3.23  apply (induct l)
    3.24  apply (rule_tac x="[]" in exI, simp, clarsimp)
    3.25 -apply (subgoal_tac "EX l.  kparts {a} = set l & cnb l = crypt_nb a", clarify)
    3.26 -apply (rule_tac x="l@l'" in exI, simp)
    3.27 +apply (subgoal_tac "EX l''.  kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
    3.28 +apply (rule_tac x="l''@l'" in exI, simp)
    3.29  apply (rule kparts_insert_substI, simp)
    3.30  by (rule kparts_msg_set)
    3.31  
     4.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Oct 11 07:39:19 2004 +0200
     4.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Mon Oct 11 07:42:22 2004 +0200
     4.3 @@ -528,7 +528,7 @@
     4.4  
     4.5  lemma last_length2 [rule_format]: "xs\<noteq>[] \<longrightarrow> (last xs)=(xs!(length xs - (Suc 0)))"
     4.6  apply(induct xs,simp+)
     4.7 -apply(case_tac "length list",simp+)
     4.8 +apply(case_tac "length xs",simp+)
     4.9  done
    4.10  
    4.11  lemma last_drop: "Suc m<length x \<Longrightarrow> last(drop (Suc m) x) = last x"
     5.1 --- a/src/HOL/HoareParallel/RG_Tran.thy	Mon Oct 11 07:39:19 2004 +0200
     5.2 +++ b/src/HOL/HoareParallel/RG_Tran.thy	Mon Oct 11 07:42:22 2004 +0200
     5.3 @@ -129,7 +129,7 @@
     5.4  lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
     5.5  apply simp
     5.6  apply(induct xs,simp+)
     5.7 -apply(case_tac list)
     5.8 +apply(case_tac xs)
     5.9  apply simp_all
    5.10  done
    5.11  
     6.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Oct 11 07:39:19 2004 +0200
     6.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Mon Oct 11 07:42:22 2004 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  *)
     6.5  
     6.6  theory SEQ
     6.7 -imports NatStar HyperPow
     6.8 +imports NatStar
     6.9  begin
    6.10  
    6.11  constdefs
    6.12 @@ -739,12 +739,12 @@
    6.13       "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
    6.14  apply (induct M)
    6.15  apply (rule_tac x = 0 in exI, simp, safe)
    6.16 -apply (cut_tac x = "\<bar>X (Suc n)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
    6.17 +apply (cut_tac x = "\<bar>X (Suc M)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
    6.18  apply safe
    6.19  apply (rule_tac x = m in exI)
    6.20  apply (rule_tac [2] x = m in exI)
    6.21 -apply (rule_tac [3] x = "Suc n" in exI, simp_all, safe)
    6.22 -apply (erule_tac [!] m1 = na in le_imp_less_or_eq [THEN disjE]) 
    6.23 +apply (rule_tac [3] x = "Suc M" in exI, simp_all, safe)
    6.24 +apply (erule_tac [!] m1 = n in le_imp_less_or_eq [THEN disjE]) 
    6.25  apply (simp_all add: less_Suc_cancel_iff)
    6.26  apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
    6.27  done
     7.1 --- a/src/HOL/Lambda/Type.thy	Mon Oct 11 07:39:19 2004 +0200
     7.2 +++ b/src/HOL/Lambda/Type.thy	Mon Oct 11 07:42:22 2004 +0200
     7.3 @@ -121,7 +121,7 @@
     7.4    apply (case_tac Ts)
     7.5    apply simp+
     7.6    apply (case_tac Ts)
     7.7 -  apply (case_tac "list @ [t]")
     7.8 +  apply (case_tac "ts @ [t]")
     7.9    apply simp+
    7.10    done
    7.11  
    7.12 @@ -185,7 +185,7 @@
    7.13    apply simp
    7.14    apply (erule_tac x = "t \<degree> a" in allE)
    7.15    apply (erule_tac x = T in allE)
    7.16 -  apply (erule_tac x = lista in allE)
    7.17 +  apply (erule_tac x = list in allE)
    7.18    apply (erule impE)
    7.19     apply (erule conjE)
    7.20     apply (erule typing.App)
     8.1 --- a/src/HOL/Lambda/WeakNorm.thy	Mon Oct 11 07:39:19 2004 +0200
     8.2 +++ b/src/HOL/Lambda/WeakNorm.thy	Mon Oct 11 07:42:22 2004 +0200
     8.3 @@ -83,14 +83,14 @@
     8.4  lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
     8.5    apply (induct m)
     8.6    apply (case_tac n)
     8.7 -  apply (case_tac [3] na)
     8.8 +  apply (case_tac [3] n)
     8.9    apply (simp only: nat.simps, rules?)+
    8.10    done
    8.11  
    8.12  lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
    8.13    apply (induct m)
    8.14    apply (case_tac n)
    8.15 -  apply (case_tac [3] na)
    8.16 +  apply (case_tac [3] n)
    8.17    apply (simp del: simp_thms, rules?)+
    8.18    done
    8.19  
     9.1 --- a/src/HOL/List.thy	Mon Oct 11 07:39:19 2004 +0200
     9.2 +++ b/src/HOL/List.thy	Mon Oct 11 07:42:22 2004 +0200
     9.3 @@ -1007,7 +1007,7 @@
     9.4  lemma take_take [simp]: "!!xs n. take n (take m xs) = take (min n m) xs"
     9.5  apply (induct m, auto)
     9.6  apply (case_tac xs, auto)
     9.7 -apply (case_tac na, auto)
     9.8 +apply (case_tac n, auto)
     9.9  done
    9.10  
    9.11  lemma drop_drop [simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs"
    10.1 --- a/src/HOL/Matrix/Float.thy	Mon Oct 11 07:39:19 2004 +0200
    10.2 +++ b/src/HOL/Matrix/Float.thy	Mon Oct 11 07:42:22 2004 +0200
    10.3 @@ -25,7 +25,7 @@
    10.4      apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
    10.5      apply (auto simp add: h)
    10.6      apply arith
    10.7 -    done  
    10.8 +    done
    10.9    show ?thesis
   10.10    proof (induct a)
   10.11      case (1 n)
   10.12 @@ -38,7 +38,7 @@
   10.13        apply (subst pow2_neg[of "-1 - int n"])
   10.14        apply (auto simp add: g pos)
   10.15        done
   10.16 -  qed  
   10.17 +  qed
   10.18  qed
   10.19    
   10.20  lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
   10.21 @@ -54,10 +54,10 @@
   10.22    qed
   10.23  next
   10.24    case (2 n)
   10.25 -  show ?case 
   10.26 +  show ?case
   10.27    proof (induct n)
   10.28      case 0
   10.29 -    show ?case 
   10.30 +    show ?case
   10.31        apply (auto)
   10.32        apply (subst pow2_neg[of "a + -1"])
   10.33        apply (subst pow2_neg[of "-1"])
   10.34 @@ -68,7 +68,7 @@
   10.35        apply (simp)
   10.36        done
   10.37      case (Suc m)
   10.38 -    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith	
   10.39 +    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
   10.40      have b: "int m - -2 = 1 + (int m + 1)" by arith
   10.41      show ?case
   10.42        apply (auto)
    11.1 --- a/src/HOL/Matrix/MatrixGeneral.thy	Mon Oct 11 07:39:19 2004 +0200
    11.2 +++ b/src/HOL/Matrix/MatrixGeneral.thy	Mon Oct 11 07:42:22 2004 +0200
    11.3 @@ -1064,7 +1064,7 @@
    11.4      apply (induct m, simp)
    11.5      apply (simp)
    11.6      apply (insert tworows)
    11.7 -    apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) na) else (A (Suc na) i))" in spec)
    11.8 +    apply (drule_tac x="% j i. (if j = 0 then (foldseq_transposed g (\<lambda>u. A u i) m) else (A (Suc m) i))" in spec)
    11.9      by (simp add: foldmatrix_def foldmatrix_transposed_def)
   11.10  qed
   11.11  
    12.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Mon Oct 11 07:39:19 2004 +0200
    12.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Mon Oct 11 07:42:22 2004 +0200
    12.3 @@ -124,7 +124,7 @@
    12.4    apply (simp only: Rep_matrix_inject[symmetric])
    12.5    apply (rule ext)+
    12.6    apply auto
    12.7 -  apply (subgoal_tac "Rep_matrix (sparse_row_vector list) 0 a = 0")
    12.8 +  apply (subgoal_tac "Rep_matrix (sparse_row_vector v) 0 a = 0")
    12.9    apply (simp)
   12.10    apply (rule sorted_sparse_row_vector_zero)
   12.11    apply auto
   12.12 @@ -135,9 +135,7 @@
   12.13    apply (induct v)
   12.14    apply (simp)
   12.15    apply (frule sorted_spvec_cons1, simp)
   12.16 -  apply (simp add: sorted_spvec.simps)
   12.17 -  apply (case_tac list)
   12.18 -  apply (simp_all)
   12.19 +  apply (simp add: sorted_spvec.simps split:list.split_asm)
   12.20    done
   12.21  
   12.22  lemma sorted_spvec_abs_spvec:
   12.23 @@ -145,9 +143,7 @@
   12.24    apply (induct v)
   12.25    apply (simp)
   12.26    apply (frule sorted_spvec_cons1, simp)
   12.27 -  apply (simp add: sorted_spvec.simps)
   12.28 -  apply (case_tac list)
   12.29 -  apply (simp_all)
   12.30 +  apply (simp add: sorted_spvec.simps split:list.split_asm)
   12.31    done
   12.32    
   12.33  defs
   12.34 @@ -193,9 +189,7 @@
   12.35  lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
   12.36    apply (auto simp add: smult_spvec_def)
   12.37    apply (induct a)
   12.38 -  apply (auto simp add: sorted_spvec.simps)
   12.39 -  apply (case_tac list)
   12.40 -  apply (auto)
   12.41 +  apply (auto simp add: sorted_spvec.simps split:list.split_asm)
   12.42    done
   12.43  
   12.44  lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr); 
   12.45 @@ -370,7 +364,7 @@
   12.46    apply (induct A)
   12.47    apply (auto)
   12.48    apply (drule sorted_spvec_cons1, simp)
   12.49 -  apply (case_tac list)
   12.50 +  apply (case_tac A)
   12.51    apply (auto simp add: sorted_spvec.simps)
   12.52    done
   12.53  
   12.54 @@ -821,18 +815,14 @@
   12.55    apply (induct A)
   12.56    apply (simp)
   12.57    apply (frule sorted_spvec_cons1, simp)
   12.58 -  apply (simp add: sorted_spvec.simps)
   12.59 -  apply (case_tac list)
   12.60 -  apply (simp_all)
   12.61 +  apply (simp add: sorted_spvec.simps split:list.split_asm)
   12.62    done 
   12.63  
   12.64  lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)" 
   12.65    apply (induct A)
   12.66    apply (simp)
   12.67    apply (frule sorted_spvec_cons1, simp)
   12.68 -  apply (simp add: sorted_spvec.simps)
   12.69 -  apply (case_tac list)
   12.70 -  apply (simp_all)
   12.71 +  apply (simp add: sorted_spvec.simps split:list.split_asm)
   12.72    done
   12.73  
   12.74  lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)"
    13.1 --- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Oct 11 07:39:19 2004 +0200
    13.2 +++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Oct 11 07:42:22 2004 +0200
    13.3 @@ -521,7 +521,7 @@
    13.4  apply (case_tac lvals) apply simp
    13.5  apply (simp (no_asm_simp) )
    13.6  
    13.7 -apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
    13.8 +apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ list" in progression_transitive, rule HOL.refl)
    13.9  apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
   13.10  apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
   13.11  apply (rule progression_one_step)
    14.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Oct 11 07:39:19 2004 +0200
    14.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Oct 11 07:42:22 2004 +0200
    14.3 @@ -116,7 +116,7 @@
    14.4  apply (clarify)
    14.5  apply (drule_tac x=kr in spec)
    14.6  apply (simp only: rev.simps)
    14.7 -apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev list @ [a])) = empty (rev kr[\<mapsto>]rev list)([k'][\<mapsto>][a])")
    14.8 +apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
    14.9  apply (simp only:)
   14.10  apply (case_tac "k' = k")
   14.11  apply simp
   14.12 @@ -1531,9 +1531,9 @@
   14.13  apply (induct m)
   14.14  apply simp
   14.15  apply (intro strip)
   14.16 -apply (subgoal_tac "na \<le> n \<or> na = Suc n")
   14.17 +apply (subgoal_tac "n \<le> m \<or> n = Suc m")
   14.18  apply (erule disjE)
   14.19 -apply (frule_tac x=na in spec, drule_tac x=xs in spec, drule mp, assumption)
   14.20 +apply (frule_tac x=n in spec, drule_tac x=xs in spec, drule mp, assumption)
   14.21  apply (rule set_drop_Suc [THEN subset_trans], assumption)
   14.22  apply auto
   14.23  done
   14.24 @@ -2310,7 +2310,7 @@
   14.25  apply (drule_tac x="lvars_pre @ [a]" in spec)
   14.26  apply (drule_tac x="lvars0" in spec)
   14.27  apply (simp (no_asm_simp) add: compInitLvars_def)
   14.28 -apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb list"
   14.29 +apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb lvars"
   14.30    in bc_mt_corresp_comb)
   14.31  apply (simp (no_asm_simp) add: compInitLvars_def)+
   14.32  
    15.1 --- a/src/HOL/NumberTheory/Chinese.thy	Mon Oct 11 07:39:19 2004 +0200
    15.2 +++ b/src/HOL/NumberTheory/Chinese.thy	Mon Oct 11 07:42:22 2004 +0200
    15.3 @@ -94,7 +94,7 @@
    15.4     apply auto
    15.5      apply (rule_tac [1] zdvd_zmult2)
    15.6      apply (rule_tac [2] zdvd_zmult)
    15.7 -    apply (subgoal_tac "i = Suc (k + n)")
    15.8 +    apply (subgoal_tac "i = Suc (k + l)")
    15.9      apply (simp_all (no_asm_simp))
   15.10    done
   15.11  
   15.12 @@ -125,11 +125,11 @@
   15.13     apply clarify
   15.14     apply (subgoal_tac "k = j")
   15.15      apply (simp_all (no_asm_simp))
   15.16 -  apply (case_tac "Suc (k + n) = j")
   15.17 -   apply (subgoal_tac "funsum f k n = 0")
   15.18 +  apply (case_tac "Suc (k + l) = j")
   15.19 +   apply (subgoal_tac "funsum f k l = 0")
   15.20      apply (rule_tac [2] funsum_zero)
   15.21 -    apply (subgoal_tac [3] "f (Suc (k + n)) = 0")
   15.22 -     apply (subgoal_tac [3] "j \<le> k + n")
   15.23 +    apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
   15.24 +     apply (subgoal_tac [3] "j \<le> k + l")
   15.25        prefer 4
   15.26        apply arith
   15.27       apply auto
    16.1 --- a/src/HOL/NumberTheory/Factorization.thy	Mon Oct 11 07:39:19 2004 +0200
    16.2 +++ b/src/HOL/NumberTheory/Factorization.thy	Mon Oct 11 07:42:22 2004 +0200
    16.3 @@ -149,7 +149,7 @@
    16.4  
    16.5  lemma nondec_oinsert [rule_format]: "nondec xs --> nondec (oinsert x xs)"
    16.6    apply (induct xs)
    16.7 -   apply (case_tac [2] list)
    16.8 +   apply (case_tac [2] xs)
    16.9      apply (simp_all cong del: list.weak_case_cong)
   16.10    done
   16.11  
   16.12 @@ -167,11 +167,11 @@
   16.13    apply (induct xs)
   16.14     apply safe
   16.15      apply simp_all
   16.16 -   apply (case_tac list)
   16.17 +   apply (case_tac xs)
   16.18      apply simp_all
   16.19 -  apply (case_tac list)
   16.20 +  apply (case_tac xs)
   16.21     apply simp
   16.22 -  apply (rule_tac y = aa and ys = lista in x_less_y_oinsert)
   16.23 +  apply (rule_tac y = aa and ys = list in x_less_y_oinsert)
   16.24     apply simp_all
   16.25    done
   16.26  
    17.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Mon Oct 11 07:39:19 2004 +0200
    17.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Mon Oct 11 07:42:22 2004 +0200
    17.3 @@ -136,7 +136,7 @@
    17.4      "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
    17.5    apply (induct z)
    17.6     apply (auto simp add: zpower_zadd_distrib)
    17.7 -  apply (subgoal_tac "zcong (x^y * x^(y * n)) (1 * 1) p")
    17.8 +  apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
    17.9     apply (rule_tac [2] zcong_zmult, simp_all)
   17.10    done
   17.11  
    18.1 --- a/src/HOL/UNITY/Transformers.thy	Mon Oct 11 07:39:19 2004 +0200
    18.2 +++ b/src/HOL/UNITY/Transformers.thy	Mon Oct 11 07:42:22 2004 +0200
    18.3 @@ -403,21 +403,21 @@
    18.4  
    18.5  lemma wens_single_finite_subset_wens_single:
    18.6        "wens_single_finite act B k \<subseteq> wens_single act B"
    18.7 -by (simp add: wens_single_eq_Union, blast) 
    18.8 +by (simp add: wens_single_eq_Union, blast)
    18.9  
   18.10  lemma subset_wens_single_finite:
   18.11        "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
   18.12         ==> \<exists>m. \<Union>W = wens_single_finite act B m"
   18.13  apply (induct k)
   18.14 - apply (rule_tac x=0 in exI, simp, blast) 
   18.15 -apply (auto simp add: atMost_Suc) 
   18.16 -apply (case_tac "wens_single_finite act B (Suc n) \<in> W") 
   18.17 - prefer 2 apply blast 
   18.18 -apply (drule_tac x="Suc n" in spec)
   18.19 + apply (rule_tac x=0 in exI, simp, blast)
   18.20 +apply (auto simp add: atMost_Suc)
   18.21 +apply (case_tac "wens_single_finite act B (Suc k) \<in> W")
   18.22 + prefer 2 apply blast
   18.23 +apply (drule_tac x="Suc k" in spec)
   18.24  apply (erule notE, rule equalityI)
   18.25 - prefer 2 apply blast 
   18.26 -apply (subst wens_single_finite_eq_Union) 
   18.27 -apply (simp add: atMost_Suc, blast) 
   18.28 + prefer 2 apply blast
   18.29 +apply (subst wens_single_finite_eq_Union)
   18.30 +apply (simp add: atMost_Suc, blast)
   18.31  done
   18.32  
   18.33  text{*lemma for Union case*}
    19.1 --- a/src/HOL/W0/W0.thy	Mon Oct 11 07:39:19 2004 +0200
    19.2 +++ b/src/HOL/W0/W0.thy	Mon Oct 11 07:42:22 2004 +0200
    19.3 @@ -890,7 +890,7 @@
    19.4    apply (tactic "safe_tac HOL_cs")
    19.5      apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
    19.6     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
    19.7 -  apply (drule_tac e = expr1 in sym [THEN W_var_geD])
    19.8 +  apply (drule_tac e = e1 in sym [THEN W_var_geD])
    19.9    apply (drule new_tv_subst_tel, assumption)
   19.10    apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
   19.11    apply (drule new_tv_subst_tel, assumption)