diff -r c5e79df8cc21 -r 084330e2ec5e src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Thu Jan 22 14:51:08 2015 +0100
+++ b/src/HOL/Probability/Probability_Measure.thy	Fri Jan 23 12:37:23 2015 +0100
@@ -145,11 +145,6 @@
   using nn_integral_mono_AE[of "\<lambda>x. c" f M] emeasure_space_1
   by (simp add: nn_integral_const_If split: split_if_asm)
 
-lemma (in prob_space) nn_integral_le_const:
-  "0 \<le> c \<Longrightarrow> (AE x in M. f x \<le> c) \<Longrightarrow> (\<integral>\<^sup>+x. f x \<partial>M) \<le> c"
-  using nn_integral_mono_AE[of f "\<lambda>x. c" M] emeasure_space_1
-  by (simp add: nn_integral_const_If split: split_if_asm)
-
 lemma (in prob_space) expectation_less:
   fixes X :: "_ \<Rightarrow> real"
   assumes [simp]: "integrable M X"