| changeset 70643 | 93a7a85de312 |
| parent 70642 | de9c4ed2d5df |
| child 71031 | 66c025383422 |
--- 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