--- a/src/HOL/Imperative_HOL/ex/Sublist.thy Fri Feb 25 08:46:52 2011 +0100
+++ b/src/HOL/Imperative_HOL/ex/Sublist.thy Fri Feb 25 14:25:41 2011 +0100
@@ -421,11 +421,6 @@
apply (induct xs arbitrary: a i j)
apply simp
apply simp
-apply (case_tac j)
-apply simp
-apply auto
-apply (case_tac nat)
-apply auto
done
(* suffices that j \<le> length xs and length ys *)
@@ -443,7 +438,6 @@
apply (case_tac i', auto)
apply (erule_tac x="Suc i'" in allE, auto)
apply (erule_tac x="i' - 1" in allE, auto)
- apply (case_tac i', auto)
apply (erule_tac x="Suc i'" in allE, auto)
done
qed
@@ -459,11 +453,9 @@
lemma nth_sublist': "\<lbrakk> k < j - i; j \<le> length xs \<rbrakk> \<Longrightarrow> (sublist' i j xs) ! k = xs ! (i + k)"
apply (induct xs arbitrary: i j k)
-apply auto
+apply simp
apply (case_tac k)
apply auto
-apply (case_tac i)
-apply auto
done
lemma set_sublist': "set (sublist' i j xs) = {x. \<exists>k. i \<le> k \<and> k < j \<and> k < List.length xs \<and> x = xs ! k}"