src/HOL/Multivariate_Analysis/Extension.thy

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