# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1601920121 -3600
# Node ID 15ea20d8a4d63201272a28291dfbeef05921e6e2
# Parent  becf08cb81e1246f8267203cf38246ba692940c2
A few more reversions

diff -r becf08cb81e1 -r 15ea20d8a4d6 src/HOL/Complex_Analysis/Cauchy_Integral_Theorem.thy
--- 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)"
diff -r becf08cb81e1 -r 15ea20d8a4d6 src/HOL/Complex_Analysis/Winding_Numbers.thy
--- 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)