--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Oct 10 12:12:23 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Oct 10 12:12:23 2012 +0200
@@ -569,7 +569,6 @@
by (simp_all add: borel_eq_atLeastAtMost sets_eq)
show "range cube \<subseteq> ?E" unfolding cube_def [abs_def] by auto
- show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
{ fix x :: 'a have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
then show "(\<Union>i. cube i :: 'a set) = UNIV" by auto