--- a/src/HOL/Probability/Measure.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Probability/Measure.thy Mon Sep 12 07:55:43 2011 +0200
@@ -940,7 +940,7 @@
proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
- using F by fastsimp
+ using F by fastforce
next
fix n
have "\<mu> (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. \<mu> (F i))" using F