diff -r f30e941b4512 -r 6b1c0a80a57a src/HOL/Probability/Lebesgue_Measure.thy
--- a/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 13 16:40:06 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Tue Mar 13 16:56:56 2012 +0100
@@ -48,7 +48,7 @@
 qed
 
 lemma cube_subset_Suc[intro]: "cube n \<subseteq> cube (Suc n)"
-  unfolding cube_def_raw subset_eq apply safe unfolding mem_interval by auto
+  unfolding cube_def subset_eq apply safe unfolding mem_interval apply auto done
 
 subsection {* Lebesgue measure *} 
 
@@ -95,7 +95,7 @@
     using A by (auto intro!: integrable_sub dest: lebesgueD simp: cube_def)
 next
   fix n show "(indicator {} :: _\<Rightarrow>real) integrable_on cube n"
-    by (auto simp: cube_def indicator_def_raw)
+    by (auto simp: cube_def indicator_def [abs_def])
 next
   fix A :: "nat \<Rightarrow> 'a set" and n ::nat assume "range A \<subseteq> sets lebesgue"
   then have A: "\<And>i. (indicator (A i) :: _ \<Rightarrow> real) integrable_on cube n"
@@ -193,7 +193,7 @@
   have "(?I has_integral content ?R) (cube n) \<longleftrightarrow> (indicator ?R has_integral content ?R) UNIV"
     unfolding has_integral_restrict_univ[where s="cube n", symmetric] by simp
   also have "\<dots> \<longleftrightarrow> ((\<lambda>x. 1) has_integral content ?R) ?R"
-    unfolding indicator_def_raw has_integral_restrict_univ ..
+    unfolding indicator_def [abs_def] has_integral_restrict_univ ..
   finally show ?thesis
     using has_integral_const[of "1::real" "?N" "?P"] by simp
 qed
@@ -437,9 +437,9 @@
   shows lmeasure_atLeastAtMost[simp]: "lebesgue.\<mu> {a..b} = ereal (content {a..b})"
 proof -
   have "(indicator (UNIV \<inter> {a..b})::_\<Rightarrow>real) integrable_on UNIV"
-    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def_raw)
+    unfolding integrable_indicator_UNIV by (simp add: integrable_const indicator_def [abs_def])
   from lmeasure_eq_integral[OF this] show ?thesis unfolding integral_indicator_UNIV
-    by (simp add: indicator_def_raw)
+    by (simp add: indicator_def [abs_def])
 qed
 
 lemma atLeastAtMost_singleton_euclidean[simp]:
@@ -504,7 +504,7 @@
   and sets_lborel[simp]: "sets lborel = sets borel"
   and measure_lborel[simp]: "measure lborel = lebesgue.\<mu>"
   and measurable_lborel[simp]: "measurable lborel = measurable borel"
-  by (simp_all add: measurable_def_raw lborel_def)
+  by (simp_all add: measurable_def [abs_def] lborel_def)
 
 interpretation lborel: measure_space "lborel :: ('a::ordered_euclidean_space) measure_space"
   where "space lborel = UNIV"
@@ -871,7 +871,7 @@
 
   let ?E = "\<lparr> space = UNIV :: 'a set, sets = range (\<lambda>(a,b). {a..b}) \<rparr>"
   show "Int_stable ?E" using Int_stable_cuboids .
-  show "range cube \<subseteq> sets ?E" unfolding cube_def_raw by auto
+  show "range cube \<subseteq> sets ?E" unfolding cube_def [abs_def] by auto
   show "incseq cube" using cube_subset_Suc by (auto intro!: incseq_SucI)
   { fix x have "\<exists>n. x \<in> cube n" using mem_big_cube[of x] by fastforce }
   then show "(\<Union>i. cube i) = space ?E" by auto
@@ -1001,7 +1001,7 @@
     then show "(\<Union>i. cube i) = space ?E" by auto
     show "incseq cube" by (intro incseq_SucI cube_subset_Suc)
     show "range cube \<subseteq> sets ?E"
-      unfolding cube_def_raw by auto
+      unfolding cube_def [abs_def] by auto
     show "\<And>i. measure lebesgue (cube i) \<noteq> \<infinity>"
       by (simp add: cube_def)
     show "measure_space lborel" by default