# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1476814360 -3600
# Node ID 1f53d58373bf5c34b62733b8bb6f02b46c2ee416
# Parent  42f28160bad92d9e1ff94a4433543269c4e89db0
Inserted necessary dependency

diff -r 42f28160bad9 -r 1f53d58373bf src/HOL/Analysis/Further_Topology.thy
--- 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>