more symbols;
authorwenzelm
Wed Dec 30 14:05:51 2015 +0100 (2015-12-30)
changeset 619763a27957ac658
parent 61975 b4b11391c676
child 61977 f55f28132128
more symbols;
NEWS
etc/abbrevs
src/HOL/Deriv.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/NSA/CLim.thy
src/HOL/NSA/HLim.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Wed Dec 30 11:37:29 2015 +0100
     1.2 +++ b/NEWS	Wed Dec 30 14:05:51 2015 +0100
     1.3 @@ -504,6 +504,7 @@
     1.4  
     1.5    notation (in topological_space) tendsto (infixr "--->" 55)
     1.6    notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
     1.7 +  notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
     1.8  
     1.9    notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
    1.10    notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
     2.1 --- a/etc/abbrevs	Wed Dec 30 11:37:29 2015 +0100
     2.2 +++ b/etc/abbrevs	Wed Dec 30 14:05:51 2015 +0100
     2.3 @@ -3,6 +3,8 @@
     2.4  (*prevent replacement of very long arrows*)
     2.5  "===>" = "===>"
     2.6  
     2.7 +"--->" = "\<midarrow>\<rightarrow>"
     2.8 +
     2.9  (*HOL-NSA*)
    2.10  "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
    2.11  "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
     3.1 --- a/src/HOL/Deriv.thy	Wed Dec 30 11:37:29 2015 +0100
     3.2 +++ b/src/HOL/Deriv.thy	Wed Dec 30 14:05:51 2015 +0100
     3.3 @@ -148,12 +148,12 @@
     3.4    by (simp add: has_derivative_at_within divide_inverse ac_simps)
     3.5  
     3.6  lemma has_derivative_at:
     3.7 -  "(f has_derivative D) (at x) \<longleftrightarrow> (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) -- 0 --> 0)"
     3.8 +  "(f has_derivative D) (at x) \<longleftrightarrow> (bounded_linear D \<and> (\<lambda>h. norm (f (x + h) - f x - D h) / norm h) \<midarrow>0\<rightarrow> 0)"
     3.9    unfolding has_derivative_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
    3.10  
    3.11  lemma field_has_derivative_at:
    3.12    fixes x :: "'a::real_normed_field"
    3.13 -  shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
    3.14 +  shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
    3.15    apply (unfold has_derivative_at)
    3.16    apply (simp add: bounded_linear_mult_right)
    3.17    apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
    3.18 @@ -454,7 +454,7 @@
    3.19    interpret F: bounded_linear F
    3.20      using assms by (rule has_derivative_bounded_linear)
    3.21    let ?r = "\<lambda>h. norm (F h) / norm h"
    3.22 -  have *: "?r -- 0 --> 0"
    3.23 +  have *: "?r \<midarrow>0\<rightarrow> 0"
    3.24      using assms unfolding has_derivative_at by simp
    3.25    show "F = (\<lambda>h. 0)"
    3.26    proof
    3.27 @@ -599,7 +599,7 @@
    3.28  lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
    3.29    by (force simp add: real_differentiable_def)
    3.30  
    3.31 -lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
    3.32 +lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
    3.33    apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
    3.34    apply (subst (2) tendsto_norm_zero_iff[symmetric])
    3.35    apply (rule filterlim_cong)
    3.36 @@ -701,7 +701,7 @@
    3.37  
    3.38  subsection \<open>Derivatives\<close>
    3.39  
    3.40 -lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
    3.41 +lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
    3.42    by (simp add: DERIV_def)
    3.43  
    3.44  lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F"
    3.45 @@ -883,8 +883,8 @@
    3.46  
    3.47  lemma DERIV_LIM_iff:
    3.48    fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" shows
    3.49 -     "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
    3.50 -      ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
    3.51 +     "((%h. (f(a + h) - f(a)) / h) \<midarrow>0\<rightarrow> D) =
    3.52 +      ((%x. (f(x)-f(a)) / (x-a)) \<midarrow>a\<rightarrow> D)"
    3.53  apply (rule iffI)
    3.54  apply (drule_tac k="- a" in LIM_offset)
    3.55  apply simp
    3.56 @@ -892,7 +892,7 @@
    3.57  apply (simp add: add.commute)
    3.58  done
    3.59  
    3.60 -lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
    3.61 +lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) \<midarrow>x\<rightarrow> D"
    3.62    by (simp add: DERIV_def DERIV_LIM_iff)
    3.63  
    3.64  lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
    3.65 @@ -1485,9 +1485,9 @@
    3.66          inverse ((f (g y) - x) / (g y - g x))"
    3.67      by (simp add: inj)
    3.68  next
    3.69 -  have "(\<lambda>z. (f z - f (g x)) / (z - g x)) -- g x --> D"
    3.70 +  have "(\<lambda>z. (f z - f (g x)) / (z - g x)) \<midarrow>g x\<rightarrow> D"
    3.71      by (rule der [unfolded DERIV_iff2])
    3.72 -  hence 1: "(\<lambda>z. (f z - x) / (z - g x)) -- g x --> D"
    3.73 +  hence 1: "(\<lambda>z. (f z - x) / (z - g x)) \<midarrow>g x\<rightarrow> D"
    3.74      using inj a b by simp
    3.75    have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x"
    3.76    proof (rule exI, safe)
    3.77 @@ -1504,10 +1504,10 @@
    3.78      also assume "y \<noteq> x"
    3.79      finally show False by simp
    3.80    qed
    3.81 -  have "(\<lambda>y. (f (g y) - x) / (g y - g x)) -- x --> D"
    3.82 +  have "(\<lambda>y. (f (g y) - x) / (g y - g x)) \<midarrow>x\<rightarrow> D"
    3.83      using cont 1 2 by (rule isCont_LIM_compose2)
    3.84    thus "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x)))
    3.85 -        -- x --> inverse D"
    3.86 +        \<midarrow>x\<rightarrow> inverse D"
    3.87      using neq by (rule tendsto_inverse)
    3.88  qed
    3.89  
     4.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Dec 30 11:37:29 2015 +0100
     4.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Dec 30 14:05:51 2015 +0100
     4.3 @@ -3596,7 +3596,7 @@
     4.4    unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
     4.5    using lim_ereal by (simp_all add: comp_def)
     4.6  
     4.7 -lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)"
     4.8 +lemma inverse_infty_ereal_tendsto_0: "inverse \<midarrow>\<infinity>\<rightarrow> (0::ereal)"
     4.9  proof -
    4.10    have **: "((\<lambda>x. ereal (inverse x)) \<longlongrightarrow> ereal 0) at_infinity"
    4.11      by (intro tendsto_intros tendsto_inverse_0)
    4.12 @@ -3609,10 +3609,10 @@
    4.13  
    4.14  lemma inverse_ereal_tendsto_pos:
    4.15    fixes x :: ereal assumes "0 < x"
    4.16 -  shows "inverse -- x --> inverse x"
    4.17 +  shows "inverse \<midarrow>x\<rightarrow> inverse x"
    4.18  proof (cases x)
    4.19    case (real r)
    4.20 -  with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
    4.21 +  with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) \<midarrow>r\<rightarrow> ereal (inverse r)"
    4.22      by (auto intro!: tendsto_inverse)
    4.23    from real \<open>0 < x\<close> show ?thesis
    4.24      by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
     5.1 --- a/src/HOL/Limits.thy	Wed Dec 30 11:37:29 2015 +0100
     5.2 +++ b/src/HOL/Limits.thy	Wed Dec 30 14:05:51 2015 +0100
     5.3 @@ -1941,40 +1941,40 @@
     5.4  
     5.5  lemma LIM_eq:
     5.6    fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
     5.7 -  shows "f -- a --> L =
     5.8 +  shows "f \<midarrow>a\<rightarrow> L =
     5.9       (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
    5.10  by (simp add: LIM_def dist_norm)
    5.11  
    5.12  lemma LIM_I:
    5.13    fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    5.14    shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
    5.15 -      ==> f -- a --> L"
    5.16 +      ==> f \<midarrow>a\<rightarrow> L"
    5.17  by (simp add: LIM_eq)
    5.18  
    5.19  lemma LIM_D:
    5.20    fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
    5.21 -  shows "[| f -- a --> L; 0<r |]
    5.22 +  shows "[| f \<midarrow>a\<rightarrow> L; 0<r |]
    5.23        ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
    5.24  by (simp add: LIM_eq)
    5.25  
    5.26  lemma LIM_offset:
    5.27    fixes a :: "'a::real_normed_vector"
    5.28 -  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
    5.29 +  shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. f (x + k)) \<midarrow>(a - k)\<rightarrow> L"
    5.30    unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp
    5.31  
    5.32  lemma LIM_offset_zero:
    5.33    fixes a :: "'a::real_normed_vector"
    5.34 -  shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    5.35 +  shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L"
    5.36  by (drule_tac k="a" in LIM_offset, simp add: add.commute)
    5.37  
    5.38  lemma LIM_offset_zero_cancel:
    5.39    fixes a :: "'a::real_normed_vector"
    5.40 -  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
    5.41 +  shows "(\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L \<Longrightarrow> f \<midarrow>a\<rightarrow> L"
    5.42  by (drule_tac k="- a" in LIM_offset, simp)
    5.43  
    5.44  lemma LIM_offset_zero_iff:
    5.45    fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
    5.46 -  shows  "f -- a --> L \<longleftrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
    5.47 +  shows  "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L"
    5.48    using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
    5.49  
    5.50  lemma LIM_zero:
    5.51 @@ -1995,9 +1995,9 @@
    5.52  lemma LIM_imp_LIM:
    5.53    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    5.54    fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
    5.55 -  assumes f: "f -- a --> l"
    5.56 +  assumes f: "f \<midarrow>a\<rightarrow> l"
    5.57    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
    5.58 -  shows "g -- a --> m"
    5.59 +  shows "g \<midarrow>a\<rightarrow> m"
    5.60    by (rule metric_LIM_imp_LIM [OF f],
    5.61      simp add: dist_norm le)
    5.62  
    5.63 @@ -2005,23 +2005,23 @@
    5.64    fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
    5.65    assumes 1: "0 < R"
    5.66    assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
    5.67 -  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
    5.68 +  shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>a\<rightarrow> l"
    5.69  by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
    5.70  
    5.71  lemma LIM_compose2:
    5.72    fixes a :: "'a::real_normed_vector"
    5.73 -  assumes f: "f -- a --> b"
    5.74 -  assumes g: "g -- b --> c"
    5.75 +  assumes f: "f \<midarrow>a\<rightarrow> b"
    5.76 +  assumes g: "g \<midarrow>b\<rightarrow> c"
    5.77    assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
    5.78 -  shows "(\<lambda>x. g (f x)) -- a --> c"
    5.79 +  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
    5.80  by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
    5.81  
    5.82  lemma real_LIM_sandwich_zero:
    5.83    fixes f g :: "'a::topological_space \<Rightarrow> real"
    5.84 -  assumes f: "f -- a --> 0"
    5.85 +  assumes f: "f \<midarrow>a\<rightarrow> 0"
    5.86    assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
    5.87    assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
    5.88 -  shows "g -- a --> 0"
    5.89 +  shows "g \<midarrow>a\<rightarrow> 0"
    5.90  proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
    5.91    fix x assume x: "x \<noteq> a"
    5.92    have "norm (g x - 0) = g x" by (simp add: 1 x)
    5.93 @@ -2036,20 +2036,20 @@
    5.94  
    5.95  lemma LIM_isCont_iff:
    5.96    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
    5.97 -  shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
    5.98 +  shows "(f \<midarrow>a\<rightarrow> f a) = ((\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> f a)"
    5.99  by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
   5.100  
   5.101  lemma isCont_iff:
   5.102    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   5.103 -  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
   5.104 +  shows "isCont f x = (\<lambda>h. f (x + h)) \<midarrow>0\<rightarrow> f x"
   5.105  by (simp add: isCont_def LIM_isCont_iff)
   5.106  
   5.107  lemma isCont_LIM_compose2:
   5.108    fixes a :: "'a::real_normed_vector"
   5.109    assumes f [unfolded isCont_def]: "isCont f a"
   5.110 -  assumes g: "g -- f a --> l"
   5.111 +  assumes g: "g \<midarrow>f a\<rightarrow> l"
   5.112    assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
   5.113 -  shows "(\<lambda>x. g (f x)) -- a --> l"
   5.114 +  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> l"
   5.115  by (rule LIM_compose2 [OF f g inj])
   5.116  
   5.117  
   5.118 @@ -2403,7 +2403,7 @@
   5.119  text\<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110\<close>
   5.120  lemma LIM_fun_gt_zero:
   5.121    fixes f :: "real \<Rightarrow> real"
   5.122 -  shows "f -- c --> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)"
   5.123 +  shows "f \<midarrow>c\<rightarrow> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)"
   5.124  apply (drule (1) LIM_D, clarify)
   5.125  apply (rule_tac x = s in exI)
   5.126  apply (simp add: abs_less_iff)
   5.127 @@ -2411,7 +2411,7 @@
   5.128  
   5.129  lemma LIM_fun_less_zero:
   5.130    fixes f :: "real \<Rightarrow> real"
   5.131 -  shows "f -- c --> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x < 0)"
   5.132 +  shows "f \<midarrow>c\<rightarrow> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x < 0)"
   5.133  apply (drule LIM_D [where r="-l"], simp, clarify)
   5.134  apply (rule_tac x = s in exI)
   5.135  apply (simp add: abs_less_iff)
   5.136 @@ -2419,7 +2419,7 @@
   5.137  
   5.138  lemma LIM_fun_not_zero:
   5.139    fixes f :: "real \<Rightarrow> real"
   5.140 -  shows "f -- c --> l \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x \<noteq> 0)"
   5.141 +  shows "f \<midarrow>c\<rightarrow> l \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x \<noteq> 0)"
   5.142    using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
   5.143  
   5.144  end
     6.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Dec 30 11:37:29 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Dec 30 14:05:51 2015 +0100
     6.3 @@ -2552,7 +2552,7 @@
     6.4      then have "\<exists>d>0. \<forall>y. y \<noteq> x \<and> cmod (y-x) < d \<longrightarrow> cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
     6.5        using dpos by blast
     6.6    }
     6.7 -  then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) -- x --> 0"
     6.8 +  then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \<midarrow>x\<rightarrow> 0"
     6.9      by (simp add: Lim_at dist_norm inverse_eq_divide)
    6.10    show ?thesis
    6.11      apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
    6.12 @@ -5472,7 +5472,7 @@
    6.13    show "(\<lambda>u. f' u / (u - w) ^ (Suc k)) contour_integrable_on \<gamma>"
    6.14      by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
    6.15    have *: "(\<lambda>n. contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / k))
    6.16 -           --w--> contour_integral \<gamma> (\<lambda>u. f' u / (u - w) ^ (Suc k))"
    6.17 +           \<midarrow>w\<rightarrow> contour_integral \<gamma> (\<lambda>u. f' u / (u - w) ^ (Suc k))"
    6.18      by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
    6.19    have **: "contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k)) =
    6.20                (f u - f w) / (u - w) / k"
     7.1 --- a/src/HOL/NSA/CLim.thy	Wed Dec 30 11:37:29 2015 +0100
     7.2 +++ b/src/HOL/NSA/CLim.thy	Wed Dec 30 14:05:51 2015 +0100
     7.3 @@ -47,22 +47,22 @@
     7.4  (** get this result easily now **)
     7.5  lemma LIM_Re:
     7.6    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
     7.7 -  shows "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
     7.8 +  shows "f \<midarrow>a\<rightarrow> L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L)"
     7.9  by (simp add: LIM_NSLIM_iff NSLIM_Re)
    7.10  
    7.11  lemma LIM_Im:
    7.12    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
    7.13 -  shows "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
    7.14 +  shows "f \<midarrow>a\<rightarrow> L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L)"
    7.15  by (simp add: LIM_NSLIM_iff NSLIM_Im)
    7.16  
    7.17  lemma LIM_cnj:
    7.18    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
    7.19 -  shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
    7.20 +  shows "f \<midarrow>a\<rightarrow> L ==> (%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L"
    7.21  by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
    7.22  
    7.23  lemma LIM_cnj_iff:
    7.24    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
    7.25 -  shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
    7.26 +  shows "((%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L) = (f \<midarrow>a\<rightarrow> L)"
    7.27  by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
    7.28  
    7.29  lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
    7.30 @@ -84,7 +84,7 @@
    7.31  (** much, much easier standard proof **)
    7.32  lemma CLIM_CRLIM_iff:
    7.33    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
    7.34 -  shows "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
    7.35 +  shows "(f \<midarrow>x\<rightarrow> L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow> 0)"
    7.36  by (simp add: LIM_eq)
    7.37  
    7.38  (* so this is nicer nonstandard proof *)
    7.39 @@ -103,8 +103,8 @@
    7.40  
    7.41  lemma LIM_CRLIM_Re_Im_iff:
    7.42    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
    7.43 -  shows "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
    7.44 -                         (%x. Im(f x)) -- a --> Im(L))"
    7.45 +  shows "(f \<midarrow>a\<rightarrow> L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L) &
    7.46 +                         (%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L))"
    7.47  by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
    7.48  
    7.49  
     8.1 --- a/src/HOL/NSA/HLim.thy	Wed Dec 30 11:37:29 2015 +0100
     8.2 +++ b/src/HOL/NSA/HLim.thy	Wed Dec 30 14:05:51 2015 +0100
     8.3 @@ -136,7 +136,7 @@
     8.4  subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close>
     8.5  
     8.6  lemma LIM_NSLIM:
     8.7 -  assumes f: "f -- a --> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
     8.8 +  assumes f: "f \<midarrow>a\<rightarrow> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
     8.9  proof (rule NSLIM_I)
    8.10    fix x
    8.11    assume neq: "x \<noteq> star_of a"
    8.12 @@ -164,7 +164,7 @@
    8.13  qed
    8.14  
    8.15  lemma NSLIM_LIM:
    8.16 -  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f -- a --> L"
    8.17 +  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f \<midarrow>a\<rightarrow> L"
    8.18  proof (rule LIM_I)
    8.19    fix r::real assume r: "0 < r"
    8.20    have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
    8.21 @@ -190,7 +190,7 @@
    8.22      by transfer
    8.23  qed
    8.24  
    8.25 -theorem LIM_NSLIM_iff: "(f -- x --> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
    8.26 +theorem LIM_NSLIM_iff: "(f \<midarrow>x\<rightarrow> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
    8.27  by (blast intro: LIM_NSLIM NSLIM_LIM)
    8.28  
    8.29  
    8.30 @@ -215,7 +215,7 @@
    8.31  
    8.32  text\<open>Hence, NS continuity can be given
    8.33    in terms of standard limit\<close>
    8.34 -lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
    8.35 +lemma isNSCont_LIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow> (f a))"
    8.36  by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
    8.37  
    8.38  text\<open>Moreover, it's trivial now that NS continuity
     9.1 --- a/src/HOL/Real_Vector_Spaces.thy	Wed Dec 30 11:37:29 2015 +0100
     9.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 30 14:05:51 2015 +0100
     9.3 @@ -1727,31 +1727,31 @@
     9.4  
     9.5  subsubsection \<open>Limits of Functions\<close>
     9.6  
     9.7 -lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
     9.8 +lemma LIM_def: "f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space) =
     9.9       (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
    9.10          --> dist (f x) L < r)"
    9.11    unfolding tendsto_iff eventually_at by simp
    9.12  
    9.13  lemma metric_LIM_I:
    9.14    "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
    9.15 -    \<Longrightarrow> f -- (a::'a::metric_space) --> (L::'b::metric_space)"
    9.16 +    \<Longrightarrow> f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space)"
    9.17  by (simp add: LIM_def)
    9.18  
    9.19  lemma metric_LIM_D:
    9.20 -  "\<lbrakk>f -- (a::'a::metric_space) --> (L::'b::metric_space); 0 < r\<rbrakk>
    9.21 +  "\<lbrakk>f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space); 0 < r\<rbrakk>
    9.22      \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
    9.23  by (simp add: LIM_def)
    9.24  
    9.25  lemma metric_LIM_imp_LIM:
    9.26 -  assumes f: "f -- a --> (l::'a::metric_space)"
    9.27 +  assumes f: "f \<midarrow>a\<rightarrow> (l::'a::metric_space)"
    9.28    assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
    9.29 -  shows "g -- a --> (m::'b::metric_space)"
    9.30 +  shows "g \<midarrow>a\<rightarrow> (m::'b::metric_space)"
    9.31    by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp add: eventually_at_topological le)
    9.32  
    9.33  lemma metric_LIM_equal2:
    9.34    assumes 1: "0 < R"
    9.35    assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
    9.36 -  shows "g -- a --> l \<Longrightarrow> f -- (a::'a::metric_space) --> l"
    9.37 +  shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>(a::'a::metric_space)\<rightarrow> l"
    9.38  apply (rule topological_tendstoI)
    9.39  apply (drule (2) topological_tendstoD)
    9.40  apply (simp add: eventually_at, safe)
    9.41 @@ -1761,19 +1761,19 @@
    9.42  done
    9.43  
    9.44  lemma metric_LIM_compose2:
    9.45 -  assumes f: "f -- (a::'a::metric_space) --> b"
    9.46 -  assumes g: "g -- b --> c"
    9.47 +  assumes f: "f \<midarrow>(a::'a::metric_space)\<rightarrow> b"
    9.48 +  assumes g: "g \<midarrow>b\<rightarrow> c"
    9.49    assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
    9.50 -  shows "(\<lambda>x. g (f x)) -- a --> c"
    9.51 +  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
    9.52    using inj
    9.53    by (intro tendsto_compose_eventually[OF g f]) (auto simp: eventually_at)
    9.54  
    9.55  lemma metric_isCont_LIM_compose2:
    9.56    fixes f :: "'a :: metric_space \<Rightarrow> _"
    9.57    assumes f [unfolded isCont_def]: "isCont f a"
    9.58 -  assumes g: "g -- f a --> l"
    9.59 +  assumes g: "g \<midarrow>f a\<rightarrow> l"
    9.60    assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
    9.61 -  shows "(\<lambda>x. g (f x)) -- a --> l"
    9.62 +  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> l"
    9.63  by (rule metric_LIM_compose2 [OF f g inj])
    9.64  
    9.65  subsection \<open>Complete metric spaces\<close>
    10.1 --- a/src/HOL/Topological_Spaces.thy	Wed Dec 30 11:37:29 2015 +0100
    10.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Dec 30 14:05:51 2015 +0100
    10.3 @@ -1204,16 +1204,16 @@
    10.4  
    10.5  abbreviation
    10.6    LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
    10.7 -        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
    10.8 -  "f -- a --> L \<equiv> (f \<longlongrightarrow> L) (at a)"
    10.9 +        ("((_)/ \<midarrow>(_)/\<rightarrow> (_))" [60, 0, 60] 60) where
   10.10 +  "f \<midarrow>a\<rightarrow> L \<equiv> (f \<longlongrightarrow> L) (at a)"
   10.11  
   10.12 -lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
   10.13 +lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<midarrow>a\<rightarrow> l)"
   10.14    unfolding tendsto_def by (simp add: at_within_open[where S=S])
   10.15  
   10.16  lemma LIM_const_not_eq[tendsto_intros]:
   10.17    fixes a :: "'a::perfect_space"
   10.18    fixes k L :: "'b::t2_space"
   10.19 -  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
   10.20 +  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow> L"
   10.21    by (simp add: tendsto_const_iff)
   10.22  
   10.23  lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
   10.24 @@ -1221,46 +1221,46 @@
   10.25  lemma LIM_const_eq:
   10.26    fixes a :: "'a::perfect_space"
   10.27    fixes k L :: "'b::t2_space"
   10.28 -  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
   10.29 +  shows "(\<lambda>x. k) \<midarrow>a\<rightarrow> L \<Longrightarrow> k = L"
   10.30    by (simp add: tendsto_const_iff)
   10.31  
   10.32  lemma LIM_unique:
   10.33    fixes a :: "'a::perfect_space" and L M :: "'b::t2_space"
   10.34 -  shows "f -- a --> L \<Longrightarrow> f -- a --> M \<Longrightarrow> L = M"
   10.35 +  shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> f \<midarrow>a\<rightarrow> M \<Longrightarrow> L = M"
   10.36    using at_neq_bot by (rule tendsto_unique)
   10.37  
   10.38  text \<open>Limits are equal for functions equal except at limit point\<close>
   10.39  
   10.40 -lemma LIM_equal: "\<forall>x. x \<noteq> a --> (f x = g x) \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- a --> l)"
   10.41 +lemma LIM_equal: "\<forall>x. x \<noteq> a --> (f x = g x) \<Longrightarrow> (f \<midarrow>a\<rightarrow> l) \<longleftrightarrow> (g \<midarrow>a\<rightarrow> l)"
   10.42    unfolding tendsto_def eventually_at_topological by simp
   10.43  
   10.44 -lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- b --> m)"
   10.45 +lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f \<midarrow>a\<rightarrow> l) \<longleftrightarrow> (g \<midarrow>b\<rightarrow> m)"
   10.46    by (simp add: LIM_equal)
   10.47  
   10.48 -lemma LIM_cong_limit: "f -- x --> L \<Longrightarrow> K = L \<Longrightarrow> f -- x --> K"
   10.49 +lemma LIM_cong_limit: "f \<midarrow>x\<rightarrow> L \<Longrightarrow> K = L \<Longrightarrow> f \<midarrow>x\<rightarrow> K"
   10.50    by simp
   10.51  
   10.52  lemma tendsto_at_iff_tendsto_nhds:
   10.53 -  "g -- l --> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
   10.54 +  "g \<midarrow>l\<rightarrow> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
   10.55    unfolding tendsto_def eventually_at_filter
   10.56    by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
   10.57  
   10.58  lemma tendsto_compose:
   10.59 -  "g -- l --> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
   10.60 +  "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
   10.61    unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
   10.62  
   10.63 -lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
   10.64 +lemma LIM_o: "\<lbrakk>g \<midarrow>l\<rightarrow> g l; f \<midarrow>a\<rightarrow> l\<rbrakk> \<Longrightarrow> (g \<circ> f) \<midarrow>a\<rightarrow> g l"
   10.65    unfolding o_def by (rule tendsto_compose)
   10.66  
   10.67  lemma tendsto_compose_eventually:
   10.68 -  "g -- l --> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
   10.69 +  "g \<midarrow>l\<rightarrow> m \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> eventually (\<lambda>x. f x \<noteq> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> m) F"
   10.70    by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
   10.71  
   10.72  lemma LIM_compose_eventually:
   10.73 -  assumes f: "f -- a --> b"
   10.74 -  assumes g: "g -- b --> c"
   10.75 +  assumes f: "f \<midarrow>a\<rightarrow> b"
   10.76 +  assumes g: "g \<midarrow>b\<rightarrow> c"
   10.77    assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
   10.78 -  shows "(\<lambda>x. g (f x)) -- a --> c"
   10.79 +  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
   10.80    using g f inj by (rule tendsto_compose_eventually)
   10.81  
   10.82  lemma tendsto_compose_filtermap: "((g \<circ> f) \<longlongrightarrow> T) F \<longleftrightarrow> (g \<longlongrightarrow> T) (filtermap f F)"
   10.83 @@ -1280,19 +1280,19 @@
   10.84  
   10.85  lemma LIMSEQ_SEQ_conv1:
   10.86    fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   10.87 -  assumes f: "f -- a --> l"
   10.88 +  assumes f: "f \<midarrow>a\<rightarrow> l"
   10.89    shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
   10.90    using tendsto_compose_eventually [OF f, where F=sequentially] by simp
   10.91  
   10.92  lemma LIMSEQ_SEQ_conv2:
   10.93    fixes f :: "'a::first_countable_topology \<Rightarrow> 'b::topological_space"
   10.94    assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
   10.95 -  shows "f -- a --> l"
   10.96 +  shows "f \<midarrow>a\<rightarrow> l"
   10.97    using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at)
   10.98  
   10.99  lemma LIMSEQ_SEQ_conv:
  10.100    "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> (a::'a::first_countable_topology) \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L) =
  10.101 -   (X -- a --> (L::'b::topological_space))"
  10.102 +   (X \<midarrow>a\<rightarrow> (L::'b::topological_space))"
  10.103    using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
  10.104  
  10.105  lemma sequentially_imp_eventually_at_left:
  10.106 @@ -1585,7 +1585,7 @@
  10.107    continuous (at x within s) (\<lambda>x. g (f x))"
  10.108    using continuous_within_compose[of x s f g] by (simp add: comp_def)
  10.109  
  10.110 -lemma continuous_at: "continuous (at x) f \<longleftrightarrow> f -- x --> f x"
  10.111 +lemma continuous_at: "continuous (at x) f \<longleftrightarrow> f \<midarrow>x\<rightarrow> f x"
  10.112    using continuous_within[of x UNIV f] by simp
  10.113  
  10.114  lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
  10.115 @@ -1601,7 +1601,7 @@
  10.116  abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool" where
  10.117    "isCont f a \<equiv> continuous (at a) f"
  10.118  
  10.119 -lemma isCont_def: "isCont f a \<longleftrightarrow> f -- a --> f a"
  10.120 +lemma isCont_def: "isCont f a \<longleftrightarrow> f \<midarrow>a\<rightarrow> f a"
  10.121    by (rule continuous_at)
  10.122  
  10.123  lemma continuous_at_imp_continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
    11.1 --- a/src/HOL/Transcendental.thy	Wed Dec 30 11:37:29 2015 +0100
    11.2 +++ b/src/HOL/Transcendental.thy	Wed Dec 30 14:05:51 2015 +0100
    11.3 @@ -564,19 +564,19 @@
    11.4    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    11.5    assumes k: "0 < (k::real)"
    11.6      and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
    11.7 -  shows "f -- 0 --> 0"
    11.8 +  shows "f \<midarrow>0\<rightarrow> 0"
    11.9  proof (rule tendsto_norm_zero_cancel)
   11.10 -  show "(\<lambda>h. norm (f h)) -- 0 --> 0"
   11.11 +  show "(\<lambda>h. norm (f h)) \<midarrow>0\<rightarrow> 0"
   11.12    proof (rule real_tendsto_sandwich)
   11.13      show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
   11.14        by simp
   11.15      show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
   11.16        using k by (auto simp add: eventually_at dist_norm le)
   11.17 -    show "(\<lambda>h. 0) -- (0::'a) --> (0::real)"
   11.18 +    show "(\<lambda>h. 0) \<midarrow>(0::'a)\<rightarrow> (0::real)"
   11.19        by (rule tendsto_const)
   11.20 -    have "(\<lambda>h. K * norm h) -- (0::'a) --> K * norm (0::'a)"
   11.21 +    have "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> K * norm (0::'a)"
   11.22        by (intro tendsto_intros)
   11.23 -    then show "(\<lambda>h. K * norm h) -- (0::'a) --> 0"
   11.24 +    then show "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> 0"
   11.25        by simp
   11.26    qed
   11.27  qed
   11.28 @@ -586,7 +586,7 @@
   11.29    assumes k: "0 < (k::real)"
   11.30    assumes f: "summable f"
   11.31    assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
   11.32 -  shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
   11.33 +  shows "(\<lambda>h. suminf (g h)) \<midarrow>0\<rightarrow> 0"
   11.34  proof (rule lemma_termdiff4 [OF k])
   11.35    fix h::'a
   11.36    assume "h \<noteq> 0" and "norm h < k"
   11.37 @@ -615,7 +615,7 @@
   11.38    assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
   11.39      and 2: "norm x < norm K"
   11.40    shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
   11.41 -             - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   11.42 +             - of_nat n * x ^ (n - Suc 0))) \<midarrow>0\<rightarrow> 0"
   11.43  proof -
   11.44    from dense [OF 2]
   11.45    obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
   11.46 @@ -682,7 +682,7 @@
   11.47    unfolding DERIV_def
   11.48  proof (rule LIM_zero_cancel)
   11.49    show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
   11.50 -            - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
   11.51 +            - suminf (\<lambda>n. diffs c n * x^n)) \<midarrow>0\<rightarrow> 0"
   11.52    proof (rule LIM_equal2)
   11.53      show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
   11.54    next
   11.55 @@ -702,7 +702,7 @@
   11.56            (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
   11.57        by (simp add: algebra_simps)
   11.58    next
   11.59 -    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
   11.60 +    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<midarrow>0\<rightarrow> 0"
   11.61        by (rule termdiffs_aux [OF 3 4])
   11.62    qed
   11.63  qed
   11.64 @@ -4068,7 +4068,7 @@
   11.65    "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
   11.66    unfolding continuous_within by (rule tendsto_tan)
   11.67  
   11.68 -lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
   11.69 +lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) \<midarrow>pi/2\<rightarrow> 0"
   11.70    by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
   11.71  
   11.72  lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
   11.73 @@ -5572,7 +5572,7 @@
   11.74    }
   11.75    then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
   11.76      using Suc  by auto
   11.77 -  then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
   11.78 +  then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) \<midarrow>0\<rightarrow> 0"
   11.79      by (simp cong: LIM_cong)                   \<comment>\<open>the case @{term"w=0"} by continuity\<close>
   11.80    then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
   11.81      using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique