author | wenzelm |
Sun, 14 May 2017 15:35:25 +0200 | |
changeset 65823 | 4f353215888a |
parent 65822 | 17b8528c2f53 |
child 65824 | 4ff79bd2b265 |
--- 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"