--- a/src/HOL/Probability/Giry_Monad.thy Fri Nov 27 19:00:27 2015 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Sat Nov 28 23:59:08 2015 +0100
@@ -279,7 +279,6 @@
moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
ultimately show ?case
- using [[simp_trace_new]]
by simp
next
case (add f g)