src/HOL/Analysis/Brouwer_Fixpoint.thy

--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Sep 04 15:27:04 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Wed Sep 04 16:34:45 2019 +0100
@@ -15,11 +15,7 @@
 section \<open>Brouwer's Fixed Point Theorem\<close>
 
 theory Brouwer_Fixpoint
-  imports
-    Path_Connected
-    Homeomorphism
-    Continuous_Extension
-    Derivative
+  imports Homeomorphism Derivative
 begin
 
 subsection \<open>Retractions\<close>