--- a/src/HOL/Analysis/Bochner_Integration.thy Tue May 02 10:25:27 2017 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Tue May 02 14:34:06 2017 +0100
@@ -444,7 +444,7 @@
lemma simple_bochner_integral_nonneg[simp]:
fixes f :: "'a \<Rightarrow> real"
shows "(\<And>x. 0 \<le> f x) \<Longrightarrow> 0 \<le> simple_bochner_integral M f"
- by (simp add: sum_nonneg simple_bochner_integral_def)
+ by (force simp add: simple_bochner_integral_def intro: sum_nonneg)
lemma simple_bochner_integral_eq_nn_integral:
assumes f: "simple_bochner_integrable M f" "\<And>x. 0 \<le> f x"