src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy

--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue May 24 13:57:34 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Tue May 24 15:08:07 2016 +0100
@@ -19,7 +19,7 @@
 section \<open>Results connected with topological dimension.\<close>
 
 theory Brouwer_Fixpoint
-imports Path_Connected
+imports Path_Connected Homeomorphism
 begin
 
 lemma bij_betw_singleton_eq: