src/HOL/Analysis/Homeomorphism.thy

--- a/src/HOL/Analysis/Homeomorphism.thy	Mon Jan 07 14:06:54 2019 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Mon Jan 07 14:57:45 2019 +0100
@@ -5,7 +5,7 @@
 section%important \<open>Homeomorphism Theorems\<close>
 
 theory Homeomorphism
-imports Path_Connected
+imports Homotopy
 begin
 
 lemma%unimportant homeomorphic_spheres':