# HG changeset patch
# User wenzelm
# Date 1448751548 -3600
# Node ID 865bb718bdb986f8f3d9ca1623aeb7042f33087d
# Parent  814bbe5d92041448707df78e312e86a0a09e833e
removed junk;

diff -r 814bbe5d9204 -r 865bb718bdb9 src/HOL/Probability/Giry_Monad.thy
--- 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)