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 \Brouwer's Fixed Point Theorem\ theory Brouwer_Fixpoint - imports - Path_Connected - Homeomorphism - Continuous_Extension - Derivative + imports Homeomorphism Derivative begin subsection \Retractions\