# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1476815319 -3600
# Node ID bad166cb5121d00c535aeb5b4a61dd6cd086c2b6
# Parent  1f53d58373bf5c34b62733b8bb6f02b46c2ee416# Parent  fb5c74a587968612dcc23c71e74d34a1c917c7a2
Merge

diff -r fb5c74a58796 -r bad166cb5121 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Oct 18 18:48:53 2016 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue Oct 18 19:28:39 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>