src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 63918 6bf55e6e0b75
parent 63886 685fb01256af
child 63941 f353674c2528
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Sep 19 12:53:30 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Sep 19 20:06:21 2016 +0200
     1.3 @@ -951,7 +951,7 @@
     1.4        then have "cmod h * cmod ((\<Sum>i<n. f' i y) - g' y) \<le> cmod h * e"
     1.5          by (auto simp: antisym_conv2 mult_le_cancel_left norm_triangle_ineq2)
     1.6        then show "cmod ((\<Sum>i<n. h * f' i y) - g' y * h) \<le> e * cmod h"
     1.7 -        by (simp add: norm_mult [symmetric] field_simps setsum_right_distrib)
     1.8 +        by (simp add: norm_mult [symmetric] field_simps setsum_distrib_left)
     1.9      qed
    1.10    } note ** = this
    1.11    show ?thesis