changeset 71918 | 4e0a58818edc |
parent 71837 | dca11678c495 |
child 71959 | ee2c7f0dd1be |
--- a/src/HOL/Transcendental.thy Wed Jun 03 11:44:21 2020 +0200 +++ b/src/HOL/Transcendental.thy Thu Jun 04 15:30:22 2020 +0000 @@ -688,7 +688,7 @@ qed then have "\<And>p q. \<lbrakk>p < n; q < n - Suc 0\<rbrakk> \<Longrightarrow> norm ((z + h) ^ q * z ^ (n - 2 - q)) \<le> K ^ (n - 2)" - by simp + by (simp del: subst_all') then show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"