author paulson Fri, 28 Aug 2020 12:04:36 +0100 changeset 72222 01397b6e5eb0 parent 72221 98ef41a82b73 child 72223 3afe53e8b2ba
small quantifier fixes
```--- 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"])