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>