diff -r 3f7d8e05e0f2 -r 19d8a59481db src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Jan 07 14:06:54 2019 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Mon Jan 07 14:57:45 2019 +0100
@@ -15,7 +15,10 @@
 section \<open>Brouwer's Fixed Point Theorem\<close>
 
 theory Brouwer_Fixpoint
-imports Path_Connected Homeomorphism
+  imports
+    Path_Connected
+    Homeomorphism
+    Continuous_Extension
 begin
 
 (* FIXME mv topology euclidean space *)