# HG changeset patch
# User nipkow
# Date 1097473342 -7200
# Node ID f289e8ba2bb343d0f88de910dedb485edf5f8fba
# Parent  614a804d71164a0552418400a38a4f88b223e586
Proofs needed to be updated because induction now preserves name of
induction variable.

diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Auth/Guard/Extensions.thy
--- a/src/HOL/Auth/Guard/Extensions.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Auth/Guard/Extensions.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -589,11 +589,11 @@
 apply (case_tac "A=Spy", blast dest: parts_knows_Spy_subset_used)
 apply (induct evs)
 apply (simp add: used.simps, blast)
-apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify)
+apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
 apply (drule_tac P="%G. X:parts G" in knows_Cons_substD, safe)
 apply (erule initState_used)
 apply (case_tac a, auto)
-apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says)
+apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
 by (auto dest: Says_imp_used intro: used_ConsI)
 
 lemma known_max_used [rule_format]: "[| evs:p; Gets_correct p; one_step p |]
@@ -602,10 +602,10 @@
 apply (simp, blast dest: parts_knows_Spy_subset_used)
 apply (induct evs)
 apply (simp add: knows_max_def used.simps, blast)
-apply (frule_tac ev=a and evs=list in one_step_Cons, simp, clarify)
+apply (frule_tac ev=a and evs=evs in one_step_Cons, simp, clarify)
 apply (drule_tac P="%G. X:parts G" in knows_max_Cons_substD, safe)
 apply (case_tac a, auto)
-apply (drule_tac B=A and X=msg and evs=list in Gets_correct_Says)
+apply (drule_tac B=A and X=msg and evs=evs in Gets_correct_Says)
 by (auto simp: knows_max'_Cons dest: Says_imp_used intro: used_ConsI)
 
 lemma not_used_not_known: "[| evs:p; X ~:used evs;
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Auth/Guard/Guard.thy
--- a/src/HOL/Auth/Guard/Guard.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Auth/Guard/Guard.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -210,7 +210,7 @@
 
 lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
 apply (induct l, auto)
-by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp)
+by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
 
 lemma parts_cnb: "Z:parts (set l) ==>
 cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
@@ -227,15 +227,15 @@
 apply (rule_tac x="[Number nat]" in exI, simp)
 apply (rule_tac x="[Nonce nat]" in exI, simp)
 apply (rule_tac x="[Key nat]" in exI, simp)
-apply (rule_tac x="[Hash msg]" in exI, simp)
+apply (rule_tac x="[Hash X]" in exI, simp)
 apply (clarify, rule_tac x="l@la" in exI, simp)
-by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp)
+by (clarify, rule_tac x="[Crypt nat X]" in exI, simp)
 
 lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
 apply (induct l)
 apply (rule_tac x="[]" in exI, simp, clarsimp)
-apply (subgoal_tac "EX l.  kparts {a} = set l & cnb l = crypt_nb a", clarify)
-apply (rule_tac x="l@l'" in exI, simp)
+apply (subgoal_tac "EX l''.  kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
+apply (rule_tac x="l''@l'" in exI, simp)
 apply (rule kparts_insert_substI, simp)
 by (rule kparts_msg_set)
 
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Auth/Guard/GuardK.thy
--- a/src/HOL/Auth/Guard/GuardK.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Auth/Guard/GuardK.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -206,7 +206,7 @@
 
 lemma cnb_minus [simp]: "x mem l ==> cnb (minus l x) = cnb l - crypt_nb x"
 apply (induct l, auto)
-by (erule_tac l1=list and x1=x in mem_cnb_minus_substI, simp)
+by (erule_tac l1=l and x1=x in mem_cnb_minus_substI, simp)
 
 lemma parts_cnb: "Z:parts (set l) ==>
 cnb l = (cnb l - crypt_nb Z) + crypt_nb Z"
@@ -223,15 +223,15 @@
 apply (rule_tac x="[Number nat]" in exI, simp)
 apply (rule_tac x="[Nonce nat]" in exI, simp)
 apply (rule_tac x="[Key nat]" in exI, simp)
-apply (rule_tac x="[Hash msg]" in exI, simp)
+apply (rule_tac x="[Hash X]" in exI, simp)
 apply (clarify, rule_tac x="l@la" in exI, simp)
-by (clarify, rule_tac x="[Crypt nat msg]" in exI, simp)
+by (clarify, rule_tac x="[Crypt nat X]" in exI, simp)
 
 lemma kparts_set: "EX l'. kparts (set l) = set l' & cnb l' = cnb l"
 apply (induct l)
 apply (rule_tac x="[]" in exI, simp, clarsimp)
-apply (subgoal_tac "EX l.  kparts {a} = set l & cnb l = crypt_nb a", clarify)
-apply (rule_tac x="l@l'" in exI, simp)
+apply (subgoal_tac "EX l''.  kparts {a} = set l'' & cnb l'' = crypt_nb a", clarify)
+apply (rule_tac x="l''@l'" in exI, simp)
 apply (rule kparts_insert_substI, simp)
 by (rule kparts_msg_set)
 
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -528,7 +528,7 @@
 
 lemma last_length2 [rule_format]: "xs\<noteq>[] \<longrightarrow> (last xs)=(xs!(length xs - (Suc 0)))"
 apply(induct xs,simp+)
-apply(case_tac "length list",simp+)
+apply(case_tac "length xs",simp+)
 done
 
 lemma last_drop: "Suc m<length x \<Longrightarrow> last(drop (Suc m) x) = last x"
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/HoareParallel/RG_Tran.thy
--- a/src/HOL/HoareParallel/RG_Tran.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/HoareParallel/RG_Tran.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -129,7 +129,7 @@
 lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
 apply simp
 apply(induct xs,simp+)
-apply(case_tac list)
+apply(case_tac xs)
 apply simp_all
 done
 
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -6,7 +6,7 @@
 *)
 
 theory SEQ
-imports NatStar HyperPow
+imports NatStar
 begin
 
 constdefs
@@ -739,12 +739,12 @@
      "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)"
 apply (induct M)
 apply (rule_tac x = 0 in exI, simp, safe)
-apply (cut_tac x = "\<bar>X (Suc n)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
+apply (cut_tac x = "\<bar>X (Suc M)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear)
 apply safe
 apply (rule_tac x = m in exI)
 apply (rule_tac [2] x = m in exI)
-apply (rule_tac [3] x = "Suc n" in exI, simp_all, safe)
-apply (erule_tac [!] m1 = na in le_imp_less_or_eq [THEN disjE]) 
+apply (rule_tac [3] x = "Suc M" in exI, simp_all, safe)
+apply (erule_tac [!] m1 = n in le_imp_less_or_eq [THEN disjE]) 
 apply (simp_all add: less_Suc_cancel_iff)
 apply (blast intro: order_le_less_trans [THEN order_less_imp_le])
 done
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Lambda/Type.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -121,7 +121,7 @@
   apply (case_tac Ts)
   apply simp+
   apply (case_tac Ts)
-  apply (case_tac "list @ [t]")
+  apply (case_tac "ts @ [t]")
   apply simp+
   done
 
@@ -185,7 +185,7 @@
   apply simp
   apply (erule_tac x = "t \<degree> a" in allE)
   apply (erule_tac x = T in allE)
-  apply (erule_tac x = lista in allE)
+  apply (erule_tac x = list in allE)
   apply (erule impE)
    apply (erule conjE)
    apply (erule typing.App)
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -83,14 +83,14 @@
 lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
   apply (induct m)
   apply (case_tac n)
-  apply (case_tac [3] na)
+  apply (case_tac [3] n)
   apply (simp only: nat.simps, rules?)+
   done
 
 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
   apply (induct m)
   apply (case_tac n)
-  apply (case_tac [3] na)
+  apply (case_tac [3] n)
   apply (simp del: simp_thms, rules?)+
   done
 
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/List.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -1007,7 +1007,7 @@
 lemma take_take [simp]: "!!xs n. take n (take m xs) = take (min n m) xs"
 apply (induct m, auto)
 apply (case_tac xs, auto)
-apply (case_tac na, auto)
+apply (case_tac n, auto)
 done
 
 lemma drop_drop [simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs"
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Matrix/Float.thy
--- a/src/HOL/Matrix/Float.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Matrix/Float.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -25,7 +25,7 @@
     apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
     apply (auto simp add: h)
     apply arith
-    done  
+    done
   show ?thesis
   proof (induct a)
     case (1 n)
@@ -38,7 +38,7 @@
       apply (subst pow2_neg[of "-1 - int n"])
       apply (auto simp add: g pos)
       done
-  qed  
+  qed
 qed
   
 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
@@ -54,10 +54,10 @@
   qed
 next
   case (2 n)
-  show ?case 
+  show ?case
   proof (induct n)
     case 0
-    show ?case 
+    show ?case
       apply (auto)
       apply (subst pow2_neg[of "a + -1"])
       apply (subst pow2_neg[of "-1"])
@@ -68,7 +68,7 @@
       apply (simp)
       done
     case (Suc m)
-    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith	
+    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
     have b: "int m - -2 = 1 + (int m + 1)" by arith
     show ?case
       apply (auto)
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -1064,7 +1064,7 @@
     apply (induct m, simp)
     apply (simp)
     apply (insert tworows)
-    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)
+    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)
     by (simp add: foldmatrix_def foldmatrix_transposed_def)
 qed
 
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -124,7 +124,7 @@
   apply (simp only: Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply auto
-  apply (subgoal_tac "Rep_matrix (sparse_row_vector list) 0 a = 0")
+  apply (subgoal_tac "Rep_matrix (sparse_row_vector v) 0 a = 0")
   apply (simp)
   apply (rule sorted_sparse_row_vector_zero)
   apply auto
@@ -135,9 +135,7 @@
   apply (induct v)
   apply (simp)
   apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps)
-  apply (case_tac list)
-  apply (simp_all)
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
   done
 
 lemma sorted_spvec_abs_spvec:
@@ -145,9 +143,7 @@
   apply (induct v)
   apply (simp)
   apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps)
-  apply (case_tac list)
-  apply (simp_all)
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
   done
   
 defs
@@ -193,9 +189,7 @@
 lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
   apply (auto simp add: smult_spvec_def)
   apply (induct a)
-  apply (auto simp add: sorted_spvec.simps)
-  apply (case_tac list)
-  apply (auto)
+  apply (auto simp add: sorted_spvec.simps split:list.split_asm)
   done
 
 lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr); 
@@ -370,7 +364,7 @@
   apply (induct A)
   apply (auto)
   apply (drule sorted_spvec_cons1, simp)
-  apply (case_tac list)
+  apply (case_tac A)
   apply (auto simp add: sorted_spvec.simps)
   done
 
@@ -821,18 +815,14 @@
   apply (induct A)
   apply (simp)
   apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps)
-  apply (case_tac list)
-  apply (simp_all)
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
   done 
 
 lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)" 
   apply (induct A)
   apply (simp)
   apply (frule sorted_spvec_cons1, simp)
-  apply (simp add: sorted_spvec.simps)
-  apply (case_tac list)
-  apply (simp_all)
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
   done
 
 lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)"
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/MicroJava/Comp/CorrComp.thy
--- a/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/MicroJava/Comp/CorrComp.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -521,7 +521,7 @@
 apply (case_tac lvals) apply simp
 apply (simp (no_asm_simp) )
 
-apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ lista" in progression_transitive, rule HOL.refl)
+apply (rule_tac ?lvars1.0 = "(prfx @ [default_val (snd a)]) @ list" in progression_transitive, rule HOL.refl)
 apply (case_tac a) apply (simp (no_asm_simp) add: compInit_def)
 apply (rule_tac ?instrs0.0 = "[load_default_val b]" in progression_transitive, simp)
 apply (rule progression_one_step)
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -116,7 +116,7 @@
 apply (clarify)
 apply (drule_tac x=kr in spec)
 apply (simp only: rev.simps)
-apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev list @ [a])) = empty (rev kr[\<mapsto>]rev list)([k'][\<mapsto>][a])")
+apply (subgoal_tac "(empty(rev kr @ [k'][\<mapsto>]rev xs @ [a])) = empty (rev kr[\<mapsto>]rev xs)([k'][\<mapsto>][a])")
 apply (simp only:)
 apply (case_tac "k' = k")
 apply simp
@@ -1531,9 +1531,9 @@
 apply (induct m)
 apply simp
 apply (intro strip)
-apply (subgoal_tac "na \<le> n \<or> na = Suc n")
+apply (subgoal_tac "n \<le> m \<or> n = Suc m")
 apply (erule disjE)
-apply (frule_tac x=na in spec, drule_tac x=xs in spec, drule mp, assumption)
+apply (frule_tac x=n in spec, drule_tac x=xs in spec, drule mp, assumption)
 apply (rule set_drop_Suc [THEN subset_trans], assumption)
 apply auto
 done
@@ -2310,7 +2310,7 @@
 apply (drule_tac x="lvars_pre @ [a]" in spec)
 apply (drule_tac x="lvars0" in spec)
 apply (simp (no_asm_simp) add: compInitLvars_def)
-apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb list"
+apply (rule_tac ?bc1.0="compInit jmb a" and ?bc2.0="compInitLvars jmb lvars"
   in bc_mt_corresp_comb)
 apply (simp (no_asm_simp) add: compInitLvars_def)+
 
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/NumberTheory/Chinese.thy
--- a/src/HOL/NumberTheory/Chinese.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -94,7 +94,7 @@
    apply auto
     apply (rule_tac [1] zdvd_zmult2)
     apply (rule_tac [2] zdvd_zmult)
-    apply (subgoal_tac "i = Suc (k + n)")
+    apply (subgoal_tac "i = Suc (k + l)")
     apply (simp_all (no_asm_simp))
   done
 
@@ -125,11 +125,11 @@
    apply clarify
    apply (subgoal_tac "k = j")
     apply (simp_all (no_asm_simp))
-  apply (case_tac "Suc (k + n) = j")
-   apply (subgoal_tac "funsum f k n = 0")
+  apply (case_tac "Suc (k + l) = j")
+   apply (subgoal_tac "funsum f k l = 0")
     apply (rule_tac [2] funsum_zero)
-    apply (subgoal_tac [3] "f (Suc (k + n)) = 0")
-     apply (subgoal_tac [3] "j \<le> k + n")
+    apply (subgoal_tac [3] "f (Suc (k + l)) = 0")
+     apply (subgoal_tac [3] "j \<le> k + l")
       prefer 4
       apply arith
      apply auto
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/NumberTheory/Factorization.thy
--- a/src/HOL/NumberTheory/Factorization.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -149,7 +149,7 @@
 
 lemma nondec_oinsert [rule_format]: "nondec xs --> nondec (oinsert x xs)"
   apply (induct xs)
-   apply (case_tac [2] list)
+   apply (case_tac [2] xs)
     apply (simp_all cong del: list.weak_case_cong)
   done
 
@@ -167,11 +167,11 @@
   apply (induct xs)
    apply safe
     apply simp_all
-   apply (case_tac list)
+   apply (case_tac xs)
     apply simp_all
-  apply (case_tac list)
+  apply (case_tac xs)
    apply simp
-  apply (rule_tac y = aa and ys = lista in x_less_y_oinsert)
+  apply (rule_tac y = aa and ys = list in x_less_y_oinsert)
    apply simp_all
   done
 
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -136,7 +136,7 @@
     "[x^y = 1] (mod p) \<Longrightarrow> [x^(y * z) = 1] (mod p)"
   apply (induct z)
    apply (auto simp add: zpower_zadd_distrib)
-  apply (subgoal_tac "zcong (x^y * x^(y * n)) (1 * 1) p")
+  apply (subgoal_tac "zcong (x^y * x^(y * z)) (1 * 1) p")
    apply (rule_tac [2] zcong_zmult, simp_all)
   done
 
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -403,21 +403,21 @@
 
 lemma wens_single_finite_subset_wens_single:
       "wens_single_finite act B k \<subseteq> wens_single act B"
-by (simp add: wens_single_eq_Union, blast) 
+by (simp add: wens_single_eq_Union, blast)
 
 lemma subset_wens_single_finite:
       "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
        ==> \<exists>m. \<Union>W = wens_single_finite act B m"
 apply (induct k)
- apply (rule_tac x=0 in exI, simp, blast) 
-apply (auto simp add: atMost_Suc) 
-apply (case_tac "wens_single_finite act B (Suc n) \<in> W") 
- prefer 2 apply blast 
-apply (drule_tac x="Suc n" in spec)
+ apply (rule_tac x=0 in exI, simp, blast)
+apply (auto simp add: atMost_Suc)
+apply (case_tac "wens_single_finite act B (Suc k) \<in> W")
+ prefer 2 apply blast
+apply (drule_tac x="Suc k" in spec)
 apply (erule notE, rule equalityI)
- prefer 2 apply blast 
-apply (subst wens_single_finite_eq_Union) 
-apply (simp add: atMost_Suc, blast) 
+ prefer 2 apply blast
+apply (subst wens_single_finite_eq_Union)
+apply (simp add: atMost_Suc, blast)
 done
 
 text{*lemma for Union case*}
diff -r 614a804d7116 -r f289e8ba2bb3 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Mon Oct 11 07:39:19 2004 +0200
+++ b/src/HOL/W0/W0.thy	Mon Oct 11 07:42:22 2004 +0200
@@ -890,7 +890,7 @@
   apply (tactic "safe_tac HOL_cs")
     apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
    apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
-  apply (drule_tac e = expr1 in sym [THEN W_var_geD])
+  apply (drule_tac e = e1 in sym [THEN W_var_geD])
   apply (drule new_tv_subst_tel, assumption)
   apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
   apply (drule new_tv_subst_tel, assumption)