# HG changeset patch
# User nipkow
# Date 1574969887 -3600
# Node ID a25b6f79043f29a93f050e76f99dde01881ea995
# Parent  df1d96114754df10f6169983e9852b6b412923c0# Parent  57bc95d2349106659892a04a617bfe6a445069e1
merged

diff -r df1d96114754 -r a25b6f79043f src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Thu Nov 28 16:43:02 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Thu Nov 28 20:38:07 2019 +0100
@@ -4,7 +4,7 @@
 section\<open>Euclidean space and n-spheres, as subtopologies of n-dimensional space\<close>
 
 theory Abstract_Euclidean_Space
-imports Homotopy Locally T1_Spaces
+imports Homotopy Locally
 begin
 
 subsection \<open>Euclidean spaces as abstract topologies\<close>
diff -r df1d96114754 -r a25b6f79043f src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 28 16:43:02 2019 +0000
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 28 20:38:07 2019 +0100
@@ -5,7 +5,7 @@
 section \<open>Finite Cartesian Products of Euclidean Spaces\<close>
 
 theory Cartesian_Euclidean_Space
-imports Cartesian_Space Derivative
+imports Convex_Euclidean_Space Derivative
 begin
 
 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
diff -r df1d96114754 -r a25b6f79043f src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Thu Nov 28 16:43:02 2019 +0000
+++ b/src/HOL/Analysis/Derivative.thy	Thu Nov 28 20:38:07 2019 +0100
@@ -7,10 +7,6 @@
 
 theory Derivative
   imports
-    Convex_Euclidean_Space
-    Abstract_Limits
-    Operator_Norm
-    Uniform_Limit
     Bounded_Linear_Function
     Line_Segment
 begin