# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1466075104 -3600
# Node ID 00090a0cd17f96be4b5fca8b99cbbd25d5a05aa6
# Parent  3b69758756331faf4c267e4051862fe7f0eef9dc
Removed instances of ^ from theory markup

diff -r 3b6975875633 -r 00090a0cd17f src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- 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
diff -r 3b6975875633 -r 00090a0cd17f 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"