# HG changeset patch # User chaieb # Date 1204122942 -3600 # Node ID 8dbf0e9d93d3a5ac6bd252582274d9cdef7df3fa # Parent 34cb0b457dcca79f7c926c1d5f11d4c7606d643a Fixed dependencies for proofs -- ferrack needed diff -r 34cb0b457dcc -r 8dbf0e9d93d3 src/HOL/Complex/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Wed Feb 27 14:39:58 2008 +0100 +++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy Wed Feb 27 15:35:42 2008 +0100 @@ -6,7 +6,7 @@ header{*Fundamental Theorem of Algebra*} theory Fundamental_Theorem_Algebra - imports Univ_Poly Complex + imports Univ_Poly Dense_Linear_Order Complex begin section {* Square root of complex numbers *}