eliminated spurious Unicode;
authorwenzelm
Sun Jul 22 19:57:42 2018 +0200 (11 months ago)
changeset 686800a0e68369586
parent 68679 2a20b315a44d
child 68681 14167c321d22
eliminated spurious Unicode;
src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy
src/HOL/Real_Asymp/Real_Asymp_Examples.thy
     1.1 --- a/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy	Sun Jul 22 19:55:26 2018 +0200
     1.2 +++ b/src/HOL/Real_Asymp/Manual/Real_Asymp_Doc.thy	Sun Jul 22 19:57:42 2018 +0200
     1.3 @@ -201,7 +201,7 @@
     1.4      By default, the first three terms are output and the \<open>strict\<close> option is disabled.
     1.5  
     1.6    Note that these two commands are intended for diagnostic use only. While the central part
     1.7 -  of their implementation – finding a multiseries expansion and reading off the limit – are the
     1.8 +  of their implementation -- finding a multiseries expansion and reading off the limit -- are the
     1.9    same as in the @{method real_asymp} method and therefore trustworthy, there is a small amount
    1.10    of unverified code involved in pre-processing and printing (e.\,g.\ for reducing all the
    1.11    different options for the \<open>limit\<close> option to the @{term at_top} case).
     2.1 --- a/src/HOL/Real_Asymp/Real_Asymp_Examples.thy	Sun Jul 22 19:55:26 2018 +0200
     2.2 +++ b/src/HOL/Real_Asymp/Real_Asymp_Examples.thy	Sun Jul 22 19:57:42 2018 +0200
     2.3 @@ -100,7 +100,7 @@
     2.4    unfolding f_def by real_asymp+
     2.5  
     2.6    
     2.7 -subsection \<open>Asymptotic inequalities related to the Akra–Bazzi theorem\<close>
     2.8 +subsection \<open>Asymptotic inequalities related to the Akra--Bazzi theorem\<close>
     2.9    
    2.10  definition "akra_bazzi_asymptotic1 b hb e p x \<longleftrightarrow>
    2.11    (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))