--- a/src/HOL/Analysis/Further_Topology.thy Tue Oct 18 17:29:28 2016 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy Tue Oct 18 19:12:40 2016 +0100
@@ -3,7 +3,7 @@
text\<open>Ported from HOL Light (moretop.ml) by L C Paulson\<close>
theory Further_Topology
- imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope
+ imports Equivalence_Lebesgue_Henstock_Integration Weierstrass_Theorems Polytope Complex_Transcendental
begin
subsection\<open>A map from a sphere to a higher dimensional sphere is nullhomotopic\<close>