src/HOL/Probability/Lebesgue_Integration.thy

     using mono by auto
   moreover have "AE x in M. ereal (- g x) \<le> ereal (- f x)"
     using mono by auto
   ultimately show ?thesis using fg
     by (auto intro!: add_mono positive_integral_mono_AE real_of_ereal_positive_mono
-             simp: positive_integral_positive lebesgue_integral_def diff_minus)
+             simp: positive_integral_positive lebesgue_integral_def algebra_simps)
 qed
 
 lemma integral_mono:
   assumes "integrable M f" "integrable M g" "\<And>t. t \<in> space M \<Longrightarrow> f t \<le> g t"
   shows "integral\<^sup>L M f \<le> integral\<^sup>L M g"

 lemma integral_diff[simp, intro]:
   assumes f: "integrable M f" and g: "integrable M g"
   shows "integrable M (\<lambda>t. f t - g t)"
   and "(\<integral> t. f t - g t \<partial>M) = integral\<^sup>L M f - integral\<^sup>L M g"
   using integral_add[OF f integral_minus(1)[OF g]]
-  unfolding diff_minus integral_minus(2)[OF g]
+  unfolding integral_minus(2)[OF g]
   by auto
 
 lemma integral_indicator[simp, intro]:
   assumes "A \<in> sets M" and "(emeasure M) A \<noteq> \<infinity>"
   shows "integral\<^sup>L M (indicator A) = real (emeasure M A)" (is ?int)