author paulson Mon, 05 Oct 2020 18:48:41 +0100 changeset 72381 15ea20d8a4d6 parent 72380 becf08cb81e1 child 72382 6cacbdb53637
A few more reversions
```--- a/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 05 18:46:15 2020 +0100
+++ b/src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy	Mon Oct 05 18:48:41 2020 +0100
@@ -1365,11 +1365,11 @@
where d: "0 < d"
and p: "polynomial_function p" "path_image p \<subseteq> S"
and pi: "\<And>f. f holomorphic_on S \<Longrightarrow> contour_integral g f = contour_integral p f"
-    using contour_integral_nearby_ends [OF S \<open>path g\<close> pag] assms
+    using contour_integral_nearby_ends [OF S \<open>path g\<close> pag]
apply clarify
apply (drule_tac x=g in spec)
apply (simp only: assms)
-    apply (force simp: valid_path_polynomial_function elim: path_approx_polynomial_function)
+    apply (force simp: valid_path_polynomial_function dest: path_approx_polynomial_function)
done
then obtain p' where p': "polynomial_function p'"
"\<And>x. (p has_vector_derivative (p' x)) (at x)"```
```--- a/src/HOL/Complex_Analysis/Winding_Numbers.thy	Mon Oct 05 18:46:15 2020 +0100
+++ b/src/HOL/Complex_Analysis/Winding_Numbers.thy	Mon Oct 05 18:48:41 2020 +0100
@@ -41,8 +41,7 @@
assume e: "e>0"
obtain p where p: "polynomial_function p \<and>
pathstart p = pathstart \<gamma> \<and> pathfinish p = pathfinish \<gamma> \<and> (\<forall>t\<in>{0..1}. cmod (p t - \<gamma> t) < min e (d/2))"
-        using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "min e (d/2)"] d \<open>0<e\<close>
-        by (metis divide_pos_pos min_less_iff_conj zero_less_numeral)
+        using path_approx_polynomial_function [OF \<open>path \<gamma>\<close>, of "min e (d/2)"] d \<open>0<e\<close> by auto
have "(\<lambda>w. 1 / (w - z)) holomorphic_on UNIV - {z}"
by (auto simp: intro!: holomorphic_intros)
then have "winding_number_prop \<gamma> z e p nn"
@@ -846,8 +845,7 @@
obtain p where p: "polynomial_function p" "pathstart p = pathstart \<gamma>" "pathfinish p = pathfinish \<gamma>"
and pg1: "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> cmod (p t - \<gamma> t) < 1)"
and pge: "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> cmod (p t - \<gamma> t) < e)"
-        using path_approx_polynomial_function [OF \<gamma>, of "min 1 e"] \<open>e>0\<close>
-        by (metis atLeastAtMost_iff min_less_iff_conj zero_less_one)
+        using path_approx_polynomial_function [OF \<gamma>, of "min 1 e"] \<open>e>0\<close> by force
have pip: "path_image p \<subseteq> ball 0 (B + 1)"
using B
apply (clarsimp simp add: path_image_def dist_norm ball_def)```