# HG changeset patch
# User wenzelm
# Date 1452722548 -3600
# Node ID fae6233c5f37ca25ef5317e92b7b8a473d8721d4
# Parent  a817e4335a31f62b7cd872079f419b389730754b
eliminated spurious Unicode;

diff -r a817e4335a31 -r fae6233c5f37 src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy
--- 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)"
diff -r a817e4335a31 -r fae6233c5f37 src/HOL/Multivariate_Analysis/Integral_Test.thy
--- 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 *)