eliminated suspicious Unicode;
authorwenzelm
Tue, 29 Jan 2019 21:56:40 +0100
changeset 69769 9a3b4cca6d0b
parent 69768 facaf96cd79e
child 69770 8d548b8f63ca
eliminated suspicious Unicode;
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 -