--- a/src/HOL/List.thy Wed Aug 26 19:54:19 2009 +0200
+++ b/src/HOL/List.thy Thu Aug 27 09:28:52 2009 +0200
@@ -881,10 +881,8 @@
lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
by (induct xs) auto
-lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
-apply (induct j, simp_all)
-apply (erule ssubst, auto)
-done
+lemma set_upt [simp]: "set[i..<j] = {i..<j}"
+by (induct j) (simp_all add: atLeastLessThanSuc)
lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
@@ -3782,9 +3780,7 @@
"{n<..<m} = set [Suc n..<m]"
by auto
-lemma atLeastLessThan_upt [code_unfold]:
- "{n..<m} = set [n..<m]"
-by auto
+lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
lemma greaterThanAtMost_upt [code_unfold]:
"{n<..m} = set [Suc n..<Suc m]"
--- a/src/HOL/MicroJava/BV/Typing_Framework_err.thy Wed Aug 26 19:54:19 2009 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_err.thy Thu Aug 27 09:28:52 2009 +0200
@@ -62,15 +62,9 @@
lemma bounded_err_stepI:
"\<forall>p. p < n \<longrightarrow> (\<forall>s. ap p s \<longrightarrow> (\<forall>(q,s') \<in> set (step p s). q < n))
\<Longrightarrow> bounded (err_step n ap step) n"
-apply (unfold bounded_def)
-apply clarify
-apply (simp add: err_step_def split: err.splits)
-apply (simp add: error_def)
- apply blast
-apply (simp split: split_if_asm)
- apply (blast dest: in_map_sndD)
-apply (simp add: error_def)
-apply blast
+apply (clarsimp simp: bounded_def err_step_def split: err.splits)
+apply (simp add: error_def image_def)
+apply (blast dest: in_map_sndD)
done