tuned Analysis manual
authorimmler
Mon, 02 Dec 2019 13:41:44 -0500
changeset 71197 36961c681fed
parent 71194 26b35a97bddb
child 71198 1bf7d1acbe74
tuned Analysis manual
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