--- a/src/HOL/Probability/Bochner_Integration.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Mon Oct 20 18:33:14 2014 +0200
@@ -2335,7 +2335,7 @@
(auto split: split_indicator simp: natceiling_le_eq) }
from filterlim_cong[OF refl refl this]
have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
- by (simp add: tendsto_const)
+ by simp
have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
using conv filterlim_real_sequentially by (rule filterlim_compose)
have M_measure[simp]: "borel_measurable M = borel_measurable borel"
@@ -2439,7 +2439,7 @@
then
show "(\<lambda>i. f' i x) ----> integral\<^sup>L M (f x)"
unfolding f'_def
- by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq tendsto_const)
+ by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
qed
qed