Removal of the redundant ancestor Continuous_Extension
authorpaulson <lp15@cam.ac.uk>
Wed, 04 Sep 2019 16:34:45 +0100
changeset 70833 93a7a85de312
parent 70832 de9c4ed2d5df
child 70844 cce7a95f6e0f
Removal of the redundant ancestor Continuous_Extension
src/HOL/Analysis/Brouwer_Fixpoint.thy
src/HOL/Analysis/Retracts.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>
--- 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