src/HOL/Analysis/Change_Of_Vars.thy

         by (simp add: algebra_simps sum.distrib)
       also have "\<dots> \<le> ?B"
       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]
-                   reorient: integral_mult_right integral_mult_left)
+                   flip: 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
           assume "k \<in> {..n}"
           show "integral (T k) (\<lambda>x. k * e) \<le> integral (T k) (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"