src/HOL/Fundamental_Theorem_Algebra.thy

--- a/src/HOL/Fundamental_Theorem_Algebra.thy	Thu Feb 05 15:35:06 2009 +0100
+++ b/src/HOL/Fundamental_Theorem_Algebra.thy	Fri Feb 06 00:10:58 2009 +0000
@@ -3,7 +3,7 @@
 header{*Fundamental Theorem of Algebra*}
 
 theory Fundamental_Theorem_Algebra
-imports Polynomial Dense_Linear_Order Complex
+imports Polynomial Complex
 begin
 
 subsection {* Square root of complex numbers *}
@@ -59,7 +59,8 @@
   by (rule of_real_power [symmetric])
 
 lemma real_down2: "(0::real) < d1 \<Longrightarrow> 0 < d2 ==> EX e. 0 < e & e < d1 & e < d2"
-  apply ferrack apply arith done
+  apply (rule exI[where x = "min d1 d2 / 2"])
+  by (simp add: field_simps min_def)
 
 text{* The triangle inequality for cmod *}
 lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"