--- 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: