--- a/src/HOL/Analysis/Lebesgue_Measure.thy Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Apr 26 19:51:32 2018 +0200
@@ -283,7 +283,7 @@
also have "... \<le> (\<Sum>i\<le>n. F (r i) - F (l i)) + epsilon"
using finS Sbound Sprop by (auto intro!: add_right_mono sum_mono2)
finally have "ennreal (F b - F a) \<le> (\<Sum>i\<le>n. ennreal (F (r i) - F (l i))) + epsilon"
- using egt0 by (simp add: ennreal_plus[symmetric] sum_nonneg del: ennreal_plus)
+ using egt0 by (simp add: sum_nonneg reorient: ennreal_plus)
then show "ennreal (F b - F a) \<le> (\<Sum>i. ennreal (F (r i) - F (l i))) + (epsilon :: real)"
by (rule order_trans) (auto intro!: add_mono sum_le_suminf simp del: sum_ennreal)
qed