src/HOL/Analysis/Abstract_Euclidean_Space.thy
changeset 71170 57bc95d23491
parent 70817 dd675800469d
child 71172 575b3a818de5
--- 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>