--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Jun 16 12:05:04 2016 +0100
@@ -2298,11 +2298,13 @@
text\<open>Absolute retracts (AR), absolute neighbourhood retracts (ANR) and also
Euclidean neighbourhood retracts (ENR). We define AR and ANR by
specializing the standard definitions for a set to embedding in
-spaces of higher dimension. This turns out to be sufficient (since any set in
+spaces of higher dimension. \<close>
+
+(*This turns out to be sufficient (since any set in
R^n can be embedded as a closed subset of a convex subset of R^{n+1}) to
derive the usual definitions, but we need to split them into two
implications because of the lack of type quantifiers. Then ENR turns out
-to be equivalent to ANR plus local compactness.\<close>
+to be equivalent to ANR plus local compactness. -- JRH*)
definition AR :: "'a::topological_space set => bool"
where
--- a/src/HOL/Multivariate_Analysis/Extension.thy Wed Jun 15 15:52:24 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Extension.thy Thu Jun 16 12:05:04 2016 +0100
@@ -112,7 +112,7 @@
qed
-subsection\<open>Urysohn's lemma (for real^N, where the proof is easy using distances)\<close>
+subsection\<open>Urysohn's lemma (for Euclidean spaces, where the proof is easy using distances)\<close>
lemma Urysohn_both_ne:
assumes US: "closedin (subtopology euclidean U) S"