
diff -r de9c4ed2d5df -r 93a7a85de312 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>




