--- a/src/HOL/Probability/Probability_Measure.thy Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy Wed Feb 17 21:51:56 2016 +0100
@@ -247,7 +247,7 @@
moreover
{ fix y assume y: "y \<in> I"
with q(2) \<open>open I\<close> 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 simp del: Sup_image_eq Inf_image_eq) }
+ by (auto intro!: cSup_eq_maximum convex_le_Inf_differential image_eqI [OF _ y] simp: interior_open) }
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))"