src/HOL/Analysis/Analysis.thy

--- a/src/HOL/Analysis/Analysis.thy	Mon Dec 02 18:29:22 2019 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Mon Dec 02 13:41:44 2019 -0500
@@ -6,7 +6,6 @@
   (* Topology *)
   Connected
   Abstract_Limits
-  Abstract_Euclidean_Space
   (* Functional Analysis *)
   Elementary_Normed_Spaces
   Norm_Arith
@@ -46,6 +45,7 @@
   Simplex_Content
   FPS_Convergence
   Smooth_Paths
+  Abstract_Euclidean_Space
 begin
 
 end