--- a/src/HOL/Probability/Probability_Measure.thy Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Sun Mar 16 18:09:04 2014 +0100
@@ -159,7 +159,7 @@
moreover
{ fix y assume y: "y \<in> I"
with q(2) `open I` have "Sup ((\<lambda>x. q x + ?F x * (y - x)) ` I) = q y"
- by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI[OF _ y] simp: interior_open) }
+ by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open simp del: Sup_image_eq Inf_image_eq) }
ultimately have "q (expectation X) = Sup ((\<lambda>x. q x + ?F x * (expectation X - x)) ` I)"
by simp
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"