# HG changeset patch
# User nipkow
# Date 1574962839 -3600
# Node ID 57bc95d2349106659892a04a617bfe6a445069e1
# Parent  11e1e273eaad5cee1c8451b5554756a0bd4d9ec3
reduced imports

diff -r 11e1e273eaad -r 57bc95d23491 src/HOL/Analysis/Abstract_Euclidean_Space.thy
--- a/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Thu Nov 28 15:51:54 2019 +0000
+++ b/src/HOL/Analysis/Abstract_Euclidean_Space.thy	Thu Nov 28 18:40:39 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 11e1e273eaad -r 57bc95d23491 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 28 15:51:54 2019 +0000
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Nov 28 18:40:39 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 11e1e273eaad -r 57bc95d23491 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Thu Nov 28 15:51:54 2019 +0000
+++ b/src/HOL/Analysis/Derivative.thy	Thu Nov 28 18:40:39 2019 +0100
@@ -7,10 +7,6 @@
 
 theory Derivative
   imports
-    Convex_Euclidean_Space
-    Abstract_Limits
-    Operator_Norm
-    Uniform_Limit
     Bounded_Linear_Function
     Line_Segment
 begin