src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy

--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Apr 29 14:04:22 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Apr 30 15:28:01 2015 +0100
@@ -1200,7 +1200,7 @@
     also have "... \<le> (e * norm z) * norm z ^ Suc n"
       by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
     finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
-      by (simp add: power_Suc)
+      by simp
   qed
 qed