reduced imports draft
authornipkow
Fri, 29 Nov 2019 10:24:44 +0100
changeset 71372 2124ed113d55
parent 71371 575b3a818de5
reduced imports
src/HOL/Analysis/Retracts.thy
--- a/src/HOL/Analysis/Retracts.thy	Thu Nov 28 23:06:22 2019 +0100
+++ b/src/HOL/Analysis/Retracts.thy	Fri Nov 29 10:24:44 2019 +0100
@@ -4,7 +4,6 @@
 imports
   Brouwer_Fixpoint
   Continuous_Extension
-  Ordered_Euclidean_Space
 begin
 
 text \<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also Euclidean neighbourhood
@@ -1323,7 +1322,7 @@
   using assms by (simp add: AR_ANR ANR_Times contractible_Times)
 
 subsection\<^marker>\<open>tag unimportant\<close>\<open>Retracts and intervals in ordered euclidean space\<close>
-
+(*
 lemma ANR_interval [iff]:
   fixes a :: "'a::ordered_euclidean_space"
   shows "ANR{a..b}"
@@ -1333,7 +1332,7 @@
   fixes a :: "'a::ordered_euclidean_space"
   shows "ENR{a..b}"
   by (auto simp: interval_cbox)
-
+*)
 subsection \<open>More advanced properties of ANRs and ENRs\<close>
 
 lemma ENR_rel_frontier_convex: