# HG changeset patch
# User wenzelm
# Date 1548795400 -3600
# Node ID 9a3b4cca6d0ba2e324ab2c37c10c265b1c152662
# Parent  facaf96cd79eb40630e90c12758c7613022270f3
eliminated suspicious Unicode;

diff -r facaf96cd79e -r 9a3b4cca6d0b src/HOL/Analysis/Abstract_Topology_2.thy
--- a/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Jan 29 13:54:43 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy	Tue Jan 29 21:56:40 2019 +0100
@@ -864,7 +864,7 @@
     T \<subseteq> S \<and> continuous_on S r \<and> r ` S = T \<and> (\<forall>x \<in> T. r x = x)"
   by (force simp: retraction_def)
 
-lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp – less likely to loop\<close>
+lemma retractionE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close>
   assumes "retraction S T r"
   obtains "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
 proof (rule that)
@@ -879,7 +879,7 @@
     using that by auto
 qed
 
-lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp – less likely to loop\<close>
+lemma retract_ofE: \<comment> \<open>yields properties normalized wrt. simp -- less likely to loop\<close>
   assumes "T retract_of S"
   obtains r where "T = r ` S" "r ` S \<subseteq> S" "continuous_on S r" "\<And>x. x \<in> S \<Longrightarrow> r (r x) = r x"
 proof -