--- a/src/HOL/Probability/Lebesgue_Integration.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Mon Sep 12 07:55:43 2011 +0200
@@ -216,7 +216,7 @@
shows "simple_function M f \<longleftrightarrow> finite (f`space M) \<and> f \<in> borel_measurable M"
using simple_function_borel_measurable[of f]
borel_measurable_simple_function[of f]
- by (fastsimp simp: simple_function_def)
+ by (fastforce simp: simple_function_def)
lemma (in sigma_algebra) simple_function_const[intro, simp]:
"simple_function M (\<lambda>x. c)"
@@ -462,7 +462,7 @@
have f: "finite (f`A) \<longleftrightarrow> finite (?f`space M)"
proof cases
assume "A = space M"
- then have "f`A = ?f`space M" by (fastsimp simp: image_iff)
+ then have "f`A = ?f`space M" by (fastforce simp: image_iff)
then show ?thesis by simp
next
assume "A \<noteq> space M"