src/HOL/Analysis/Topology_Euclidean_Space.thy

--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sat Dec 29 18:40:29 2018 +0000
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sat Dec 29 20:32:09 2018 +0100
@@ -8,7 +8,7 @@
 
 theory Topology_Euclidean_Space
   imports
-    Elementary_Topology
+    Elementary_Normed_Spaces
     Linear_Algebra
     Norm_Arith
 begin