changeset 71959 | ee2c7f0dd1be |
parent 71918 | 4e0a58818edc |
child 72211 | a6cbf8ce979e |
--- a/src/HOL/Transcendental.thy Thu Jun 18 09:07:54 2020 +0000 +++ b/src/HOL/Transcendental.thy Fri Jun 19 09:46:47 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 del: subst_all') + 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))"