more symbols;
authorwenzelm
Tue Dec 29 23:40:04 2015 +0100 (2015-12-29)
changeset 61971720fa884656e
parent 61970 6226261144d7
child 61972 a70b89a3e02e
more symbols;
NEWS
etc/abbrevs
src/HOL/NSA/CLim.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HLim.thy
src/HOL/NSA/HTranscendental.thy
     1.1 --- a/NEWS	Tue Dec 29 23:20:11 2015 +0100
     1.2 +++ b/NEWS	Tue Dec 29 23:40:04 2015 +0100
     1.3 @@ -505,6 +505,7 @@
     1.4    notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
     1.5  
     1.6    notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
     1.7 +  notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
     1.8  
     1.9  * The alternative notation "\<Colon>" for type and sort constraints has been
    1.10  removed: in LaTeX document output it looks the same as "::".
     2.1 --- a/etc/abbrevs	Tue Dec 29 23:20:11 2015 +0100
     2.2 +++ b/etc/abbrevs	Tue Dec 29 23:40:04 2015 +0100
     2.3 @@ -8,3 +8,4 @@
     2.4  
     2.5  (*HOL-NSA*)
     2.6  "---->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
     2.7 +"---->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
     3.1 --- a/src/HOL/NSA/CLim.thy	Tue Dec 29 23:20:11 2015 +0100
     3.2 +++ b/src/HOL/NSA/CLim.thy	Tue Dec 29 23:40:04 2015 +0100
     3.3 @@ -36,11 +36,11 @@
     3.4  
     3.5  subsection{*Limit of Complex to Complex Function*}
     3.6  
     3.7 -lemma NSLIM_Re: "f -- a --NS> L ==> (%x. Re(f x)) -- a --NS> Re(L)"
     3.8 +lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L)"
     3.9  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff 
    3.10                hRe_hcomplex_of_complex)
    3.11  
    3.12 -lemma NSLIM_Im: "f -- a --NS> L ==> (%x. Im(f x)) -- a --NS> Im(L)"
    3.13 +lemma NSLIM_Im: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L)"
    3.14  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff 
    3.15                hIm_hcomplex_of_complex)
    3.16  
    3.17 @@ -77,7 +77,7 @@
    3.18  text""
    3.19  (** another equivalence result **)
    3.20  lemma NSCLIM_NSCRLIM_iff:
    3.21 -   "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
    3.22 +   "(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)"
    3.23  by (simp add: NSLIM_def starfun_norm
    3.24      approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
    3.25  
    3.26 @@ -89,12 +89,12 @@
    3.27  
    3.28  (* so this is nicer nonstandard proof *)
    3.29  lemma NSCLIM_NSCRLIM_iff2:
    3.30 -     "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
    3.31 +     "(f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0)"
    3.32  by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
    3.33  
    3.34  lemma NSLIM_NSCRLIM_Re_Im_iff:
    3.35 -     "(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) &
    3.36 -                            (%x. Im(f x)) -- a --NS> Im(L))"
    3.37 +     "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L) &
    3.38 +                            (%x. Im(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Im(L))"
    3.39  apply (auto intro: NSLIM_Re NSLIM_Im)
    3.40  apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
    3.41  apply (auto dest!: spec)
    3.42 @@ -111,7 +111,7 @@
    3.43  subsection{*Continuity*}
    3.44  
    3.45  lemma NSLIM_isContc_iff:
    3.46 -     "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
    3.47 +     "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
    3.48  by (rule NSLIM_h_iff)
    3.49  
    3.50  subsection{*Functions from Complex to Reals*}
     4.1 --- a/src/HOL/NSA/HDeriv.thy	Tue Dec 29 23:20:11 2015 +0100
     4.2 +++ b/src/HOL/NSA/HDeriv.thy	Tue Dec 29 23:40:04 2015 +0100
     4.3 @@ -33,10 +33,10 @@
     4.4  subsection {* Derivatives *}
     4.5  
     4.6  lemma DERIV_NS_iff:
     4.7 -      "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
     4.8 +      "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
     4.9  by (simp add: DERIV_def LIM_NSLIM_iff)
    4.10  
    4.11 -lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NS> D"
    4.12 +lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
    4.13  by (simp add: DERIV_def LIM_NSLIM_iff)
    4.14  
    4.15  lemma hnorm_of_hypreal:
    4.16 @@ -70,7 +70,7 @@
    4.17  
    4.18  text{*first equivalence *}
    4.19  lemma NSDERIV_NSLIM_iff:
    4.20 -      "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NS> D)"
    4.21 +      "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
    4.22  apply (simp add: nsderiv_def NSLIM_def, auto)
    4.23  apply (drule_tac x = xa in bspec)
    4.24  apply (rule_tac [3] ccontr)
    4.25 @@ -80,7 +80,7 @@
    4.26  
    4.27  text{*second equivalence *}
    4.28  lemma NSDERIV_NSLIM_iff2:
    4.29 -     "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --NS> D)"
    4.30 +     "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S D)"
    4.31    by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
    4.32  
    4.33  (* while we're at it! *)
    4.34 @@ -227,15 +227,15 @@
    4.35  text{*Negation of function*}
    4.36  lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
    4.37  proof (simp add: NSDERIV_NSLIM_iff)
    4.38 -  assume "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D"
    4.39 -  hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) -- 0 --NS> - D"
    4.40 +  assume "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
    4.41 +  hence deriv: "(\<lambda>h. - ((f(x+h) - f x) / h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D"
    4.42      by (rule NSLIM_minus)
    4.43    have "\<forall>h. - ((f (x + h) - f x) / h) = (- f (x + h) + f x) / h"
    4.44      by (simp add: minus_divide_left)
    4.45    with deriv
    4.46 -  have "(\<lambda>h. (- f (x + h) + f x) / h) -- 0 --NS> - D" by simp
    4.47 -  then show "(\<lambda>h. (f (x + h) - f x) / h) -- 0 --NS> D \<Longrightarrow>
    4.48 -    (\<lambda>h. (f x - f (x + h)) / h) -- 0 --NS> - D" by simp
    4.49 +  have "(\<lambda>h. (- f (x + h) + f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" by simp
    4.50 +  then show "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D \<Longrightarrow>
    4.51 +    (\<lambda>h. (f x - f (x + h)) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" by simp
    4.52  qed
    4.53  
    4.54  text{*Subtraction*}
     5.1 --- a/src/HOL/NSA/HLim.thy	Tue Dec 29 23:20:11 2015 +0100
     5.2 +++ b/src/HOL/NSA/HLim.thy	Tue Dec 29 23:40:04 2015 +0100
     5.3 @@ -13,8 +13,8 @@
     5.4  
     5.5  definition
     5.6    NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
     5.7 -            ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
     5.8 -  "f -- a --NS> L =
     5.9 +            ("((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))" [60, 0, 60] 60) where
    5.10 +  "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L =
    5.11      (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
    5.12  
    5.13  definition
    5.14 @@ -32,11 +32,11 @@
    5.15  
    5.16  lemma NSLIM_I:
    5.17    "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
    5.18 -   \<Longrightarrow> f -- a --NS> L"
    5.19 +   \<Longrightarrow> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
    5.20  by (simp add: NSLIM_def)
    5.21  
    5.22  lemma NSLIM_D:
    5.23 -  "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
    5.24 +  "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
    5.25     \<Longrightarrow> starfun f x \<approx> star_of L"
    5.26  by (simp add: NSLIM_def)
    5.27  
    5.28 @@ -45,8 +45,8 @@
    5.29  
    5.30  lemma NSLIM_mult:
    5.31    fixes l m :: "'a::real_normed_algebra"
    5.32 -  shows "[| f -- x --NS> l; g -- x --NS> m |]
    5.33 -      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
    5.34 +  shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
    5.35 +      ==> (%x. f(x) * g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l * m)"
    5.36  by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
    5.37  
    5.38  lemma starfun_scaleR [simp]:
    5.39 @@ -54,53 +54,53 @@
    5.40  by transfer (rule refl)
    5.41  
    5.42  lemma NSLIM_scaleR:
    5.43 -  "[| f -- x --NS> l; g -- x --NS> m |]
    5.44 -      ==> (%x. f(x) *\<^sub>R g(x)) -- x --NS> (l *\<^sub>R m)"
    5.45 +  "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
    5.46 +      ==> (%x. f(x) *\<^sub>R g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l *\<^sub>R m)"
    5.47  by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
    5.48  
    5.49  lemma NSLIM_add:
    5.50 -     "[| f -- x --NS> l; g -- x --NS> m |]
    5.51 -      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
    5.52 +     "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |]
    5.53 +      ==> (%x. f(x) + g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + m)"
    5.54  by (auto simp add: NSLIM_def intro!: approx_add)
    5.55  
    5.56 -lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
    5.57 +lemma NSLIM_const [simp]: "(%x. k) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S k"
    5.58  by (simp add: NSLIM_def)
    5.59  
    5.60 -lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
    5.61 +lemma NSLIM_minus: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. -f(x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S -L"
    5.62  by (simp add: NSLIM_def)
    5.63  
    5.64  lemma NSLIM_diff:
    5.65 -  "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
    5.66 +  "\<lbrakk>f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l - m)"
    5.67    by (simp only: NSLIM_add NSLIM_minus diff_conv_add_uminus)
    5.68  
    5.69 -lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
    5.70 +lemma NSLIM_add_minus: "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S m |] ==> (%x. f(x) + -g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S (l + -m)"
    5.71  by (simp only: NSLIM_add NSLIM_minus)
    5.72  
    5.73  lemma NSLIM_inverse:
    5.74    fixes L :: "'a::real_normed_div_algebra"
    5.75 -  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
    5.76 -      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
    5.77 +  shows "[| f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L;  L \<noteq> 0 |]
    5.78 +      ==> (%x. inverse(f(x))) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (inverse L)"
    5.79  apply (simp add: NSLIM_def, clarify)
    5.80  apply (drule spec)
    5.81  apply (auto simp add: star_of_approx_inverse)
    5.82  done
    5.83  
    5.84  lemma NSLIM_zero:
    5.85 -  assumes f: "f -- a --NS> l" shows "(%x. f(x) - l) -- a --NS> 0"
    5.86 +  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l" shows "(%x. f(x) - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
    5.87  proof -
    5.88 -  have "(\<lambda>x. f x - l) -- a --NS> l - l"
    5.89 +  have "(\<lambda>x. f x - l) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S l - l"
    5.90      by (rule NSLIM_diff [OF f NSLIM_const])
    5.91    thus ?thesis by simp
    5.92  qed
    5.93  
    5.94 -lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
    5.95 +lemma NSLIM_zero_cancel: "(%x. f(x) - l) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 ==> f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S l"
    5.96  apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
    5.97  apply (auto simp add: add.assoc)
    5.98  done
    5.99  
   5.100  lemma NSLIM_const_not_eq:
   5.101    fixes a :: "'a::real_normed_algebra_1"
   5.102 -  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> L"
   5.103 +  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
   5.104  apply (simp add: NSLIM_def)
   5.105  apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
   5.106  apply (simp add: hypreal_epsilon_not_zero approx_def)
   5.107 @@ -108,35 +108,35 @@
   5.108  
   5.109  lemma NSLIM_not_zero:
   5.110    fixes a :: "'a::real_normed_algebra_1"
   5.111 -  shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> 0"
   5.112 +  shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S 0"
   5.113  by (rule NSLIM_const_not_eq)
   5.114  
   5.115  lemma NSLIM_const_eq:
   5.116    fixes a :: "'a::real_normed_algebra_1"
   5.117 -  shows "(\<lambda>x. k) -- a --NS> L \<Longrightarrow> k = L"
   5.118 +  shows "(\<lambda>x. k) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L \<Longrightarrow> k = L"
   5.119  apply (rule ccontr)
   5.120  apply (blast dest: NSLIM_const_not_eq)
   5.121  done
   5.122  
   5.123  lemma NSLIM_unique:
   5.124    fixes a :: "'a::real_normed_algebra_1"
   5.125 -  shows "\<lbrakk>f -- a --NS> L; f -- a --NS> M\<rbrakk> \<Longrightarrow> L = M"
   5.126 +  shows "\<lbrakk>f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L; f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S M\<rbrakk> \<Longrightarrow> L = M"
   5.127  apply (drule (1) NSLIM_diff)
   5.128  apply (auto dest!: NSLIM_const_eq)
   5.129  done
   5.130  
   5.131  lemma NSLIM_mult_zero:
   5.132    fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
   5.133 -  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
   5.134 +  shows "[| f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0; g \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0 |] ==> (%x. f(x)*g(x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S 0"
   5.135  by (drule NSLIM_mult, auto)
   5.136  
   5.137 -lemma NSLIM_self: "(%x. x) -- a --NS> a"
   5.138 +lemma NSLIM_self: "(%x. x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S a"
   5.139  by (simp add: NSLIM_def)
   5.140  
   5.141  subsubsection {* Equivalence of @{term filterlim} and @{term NSLIM} *}
   5.142  
   5.143  lemma LIM_NSLIM:
   5.144 -  assumes f: "f -- a --> L" shows "f -- a --NS> L"
   5.145 +  assumes f: "f -- a --> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
   5.146  proof (rule NSLIM_I)
   5.147    fix x
   5.148    assume neq: "x \<noteq> star_of a"
   5.149 @@ -164,7 +164,7 @@
   5.150  qed
   5.151  
   5.152  lemma NSLIM_LIM:
   5.153 -  assumes f: "f -- a --NS> L" shows "f -- a --> L"
   5.154 +  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f -- a --> L"
   5.155  proof (rule LIM_I)
   5.156    fix r::real assume r: "0 < r"
   5.157    have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
   5.158 @@ -190,7 +190,7 @@
   5.159      by transfer
   5.160  qed
   5.161  
   5.162 -theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
   5.163 +theorem LIM_NSLIM_iff: "(f -- x --> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
   5.164  by (blast intro: LIM_NSLIM NSLIM_LIM)
   5.165  
   5.166  
   5.167 @@ -200,17 +200,17 @@
   5.168    "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
   5.169  by (simp add: isNSCont_def)
   5.170  
   5.171 -lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
   5.172 +lemma isNSCont_NSLIM: "isNSCont f a ==> f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) "
   5.173  by (simp add: isNSCont_def NSLIM_def)
   5.174  
   5.175 -lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
   5.176 +lemma NSLIM_isNSCont: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a) ==> isNSCont f a"
   5.177  apply (simp add: isNSCont_def NSLIM_def, auto)
   5.178  apply (case_tac "y = star_of a", auto)
   5.179  done
   5.180  
   5.181  text{*NS continuity can be defined using NS Limit in
   5.182      similar fashion to standard def of continuity*}
   5.183 -lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
   5.184 +lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a))"
   5.185  by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
   5.186  
   5.187  text{*Hence, NS continuity can be given
   5.188 @@ -237,7 +237,7 @@
   5.189  
   5.190  (* Prove equivalence between NS limits - *)
   5.191  (* seems easier than using standard def  *)
   5.192 -lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
   5.193 +lemma NSLIM_h_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S L)"
   5.194  apply (simp add: NSLIM_def, auto)
   5.195  apply (drule_tac x = "star_of a + x" in spec)
   5.196  apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
   5.197 @@ -249,7 +249,7 @@
   5.198  apply (auto simp add: starfun star_of_def star_n_minus star_n_add add.assoc star_n_zero_num)
   5.199  done
   5.200  
   5.201 -lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
   5.202 +lemma NSLIM_isCont_iff: "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
   5.203    by (fact NSLIM_h_iff)
   5.204  
   5.205  lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
     6.1 --- a/src/HOL/NSA/HTranscendental.thy	Tue Dec 29 23:20:11 2015 +0100
     6.2 +++ b/src/HOL/NSA/HTranscendental.thy	Tue Dec 29 23:40:04 2015 +0100
     6.3 @@ -406,7 +406,7 @@
     6.4  
     6.5  
     6.6  (*
     6.7 -Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) -- 0 --NS> ln x"
     6.8 +Goalw [NSLIM_def] "(%h. ((x powr h) - 1) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S ln x"
     6.9  *)
    6.10  
    6.11  lemma HFinite_sin [simp]: "sumhr (0, whn, %n. sin_coeff n * x ^ n) \<in> HFinite"