--- 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>
--- 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}"
--- 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