--- 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>
--- a/src/HOL/Analysis/Retracts.thy Wed Sep 04 15:27:04 2019 +0100
+++ b/src/HOL/Analysis/Retracts.thy Wed Sep 04 16:34:45 2019 +0100
@@ -1,7 +1,7 @@
section \<open>Absolute Retracts, Absolute Neighbourhood Retracts and Euclidean Neighbourhood Retracts\<close>
theory Retracts
- imports Brouwer_Fixpoint Ordered_Euclidean_Space
+ imports Brouwer_Fixpoint Continuous_Extension Ordered_Euclidean_Space
begin