--- a/src/HOL/Analysis/Retracts.thy Thu Nov 28 23:06:22 2019 +0100
+++ b/src/HOL/Analysis/Retracts.thy Fri Nov 29 11:04:47 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
@@ -1322,6 +1321,7 @@
assumes "AR S" "AR T" shows "AR(S \<times> T)"
using assms by (simp add: AR_ANR ANR_Times contractible_Times)
+(* Unused
subsection\<^marker>\<open>tag unimportant\<close>\<open>Retracts and intervals in ordered euclidean space\<close>
lemma ANR_interval [iff]:
@@ -1333,6 +1333,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>