# HG changeset patch
# User wenzelm
# Date 1532282262 -7200
# Node ID 0a0e683695862ba1b40d1f873a6de4eb9ba29799
# Parent  2a20b315a44d2e5fe82825dd544b23b719b6bf8c
eliminated spurious Unicode;

diff -r 2a20b315a44d -r 0a0e68369586 src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy
--- a/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy	Sun Jul 22 19:55:26 2018 +0200
+++ b/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy	Sun Jul 22 19:57:42 2018 +0200
@@ -201,7 +201,7 @@
     By default, the first three terms are output and the \<open>strict\<close> option is disabled.
 
   Note that these two commands are intended for diagnostic use only. While the central part
-  of their implementation – finding a multiseries expansion and reading off the limit – are the
+  of their implementation -- finding a multiseries expansion and reading off the limit -- are the
   same as in the @{method real_asymp} method and therefore trustworthy, there is a small amount
   of unverified code involved in pre-processing and printing (e.\,g.\ for reducing all the
   different options for the \<open>limit\<close> option to the @{term at_top} case).
diff -r 2a20b315a44d -r 0a0e68369586 src/HOL/Real_Asymp/Real_Asymp_Examples.thy
--- a/src/HOL/Real_Asymp/Real_Asymp_Examples.thy	Sun Jul 22 19:55:26 2018 +0200
+++ b/src/HOL/Real_Asymp/Real_Asymp_Examples.thy	Sun Jul 22 19:57:42 2018 +0200
@@ -100,7 +100,7 @@
   unfolding f_def by real_asymp+
 
   
-subsection \<open>Asymptotic inequalities related to the Akra–Bazzi theorem\<close>
+subsection \<open>Asymptotic inequalities related to the Akra--Bazzi theorem\<close>
   
 definition "akra_bazzi_asymptotic1 b hb e p x \<longleftrightarrow>
   (1 - hb * inverse b * ln x powr -(1+e)) powr p * (1 + ln (b*x + hb*x/ln x powr (1+e)) powr (-e/2))