eliminated suspicious Unicode;
authorwenzelm
Sun, 14 May 2017 15:35:25 +0200
changeset 65823 4f353215888a
parent 65822 17b8528c2f53
child 65824 4ff79bd2b265
eliminated suspicious Unicode;
src/HOL/Analysis/Great_Picard.thy
--- a/src/HOL/Analysis/Great_Picard.thy	Sun May 14 15:34:20 2017 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy	Sun May 14 15:35:25 2017 +0200
@@ -614,7 +614,7 @@
 qed
 
 
-subsection\<open>The Arzelà–Ascoli theorem\<close>
+subsection\<open>The Arzelà--Ascoli theorem\<close>
 
 lemma subsequence_diagonalization_lemma:
   fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"