# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1567611285 -3600
# Node ID 93a7a85de31218ddc608172f8bdc5a7dc6823ec2
# Parent  de9c4ed2d5df9794f4ad8c5cd5dd50fa3167eb79
Removal of the redundant ancestor Continuous_Extension

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 \<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>
diff -r de9c4ed2d5df -r 93a7a85de312 src/HOL/Analysis/Retracts.thy
--- 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