--- a/src/HOL/Analysis/Change_Of_Vars.thy Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Thu Apr 26 19:51:32 2018 +0200
@@ -1273,8 +1273,7 @@
proof (rule add_mono)
have "(\<Sum>k\<le>n. real k * e * ?\<mu> (T k)) = (\<Sum>k\<le>n. integral (T k) (\<lambda>x. k * e))"
by (simp add: lmeasure_integral [OF meas_t]
- integral_mult_right [symmetric] integral_mult_left [symmetric]
- del: integral_mult_right integral_mult_left)
+ reorient: integral_mult_right integral_mult_left)
also have "\<dots> \<le> (\<Sum>k\<le>n. integral (T k) (\<lambda>x. (abs (det (matrix (f' x))))))"
proof (rule sum_mono)
fix k