--- a/src/HOL/Analysis/ex/Approximations.thy Thu Aug 27 16:48:21 2020 +0100
+++ b/src/HOL/Analysis/ex/Approximations.thy Fri Aug 28 12:04:36 2020 +0100
@@ -99,9 +99,8 @@
from assms show "(exp x - approx) \<ge> 0"
by (intro sums_le[OF _ sums_zero sums]) auto
- have "\<forall>k. x^n * (x^k / fact (n+k)) \<le> (x^n / fact n) * (x / 2)^k"
- proof
- fix k :: nat
+ have "x^n * (x^k / fact (n+k)) \<le> (x^n / fact n) * (x / 2)^k" for k::nat
+ proof -
have "x^n * (x^k / fact (n + k)) = x^(n+k) / fact (n + k)" by (simp add: power_add)
also from assms have "\<dots> \<le> x^(n+k) / (2^k * fact n)"
by (intro divide_left_mono two_power_fact_le_fact zero_le_power) simp_all
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Aug 27 16:48:21 2020 +0100
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Fri Aug 28 12:04:36 2020 +0100
@@ -33,8 +33,7 @@
proof -
define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)"
have "isCont g z" unfolding isCont_def using is_pole_tendsto[OF pole]
- apply (subst Lim_cong_at[where b=z and y=0 and g="inverse \<circ> f"])
- by (simp_all add:g_def)
+ by (simp add: g_def cong: LIM_cong)
moreover have "continuous_on (s-{z}) f" using f_holo holomorphic_on_imp_continuous_on by auto
hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def
by (auto elim!:continuous_on_inverse simp add:non_z)