Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
eliminated spurious Unicode;
authorwenzelm
Wed, 13 Jan 2016 23:02:28 +0100
changeset 62174 fae6233c5f37
parent 62173 a817e4335a31
child 62175 8ffc4d0e652d
eliminated spurious Unicode;
src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy file | annotate | diff | comparison | revisions
src/HOL/Multivariate_Analysis/Integral_Test.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Wed Jan 13 21:44:26 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Wed Jan 13 23:02:28 2016 +0100
@@ -12,9 +12,9 @@
 begin
 
 text \<open>
-  The definition of the Harmonic Numbers and the Euler–Mascheroni constant.
+  The definition of the Harmonic Numbers and the Euler-Mascheroni constant.
   Also provides a reasonably accurate approximation of @{term "ln 2 :: real"} 
-  and the Euler–Mascheroni constant.
+  and the Euler-Mascheroni constant.
 \<close>
 
 lemma ln_2_less_1: "ln 2 < (1::real)"
--- a/src/HOL/Multivariate_Analysis/Integral_Test.thy	Wed Jan 13 21:44:26 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Integral_Test.thy	Wed Jan 13 23:02:28 2016 +0100
@@ -15,7 +15,7 @@
   
   As a useful side result, we also provide some results on the difference between
   the integral and the partial sum. (This is useful e.g. for the definition of the
-  Euler–Mascheroni constant)
+  Euler-Mascheroni constant)
 \<close>
 
 (* TODO: continuous_in \<rightarrow> integrable_on *)
isabelle