# HG changeset patch
# User wenzelm
# Date 1451480751 -3600
# Node ID 3a27957ac658bb7502b717579d231a56b7add45f
# Parent  b4b11391c67615ab425457cd12cc9362c4000680
more symbols;

diff -r b4b11391c676 -r 3a27957ac658 NEWS
--- a/NEWS	Wed Dec 30 11:37:29 2015 +0100
+++ b/NEWS	Wed Dec 30 14:05:51 2015 +0100
@@ -504,6 +504,7 @@
 
   notation (in topological_space) tendsto (infixr "--->" 55)
   notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
+  notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
 
   notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
   notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
diff -r b4b11391c676 -r 3a27957ac658 etc/abbrevs
--- a/etc/abbrevs	Wed Dec 30 11:37:29 2015 +0100
+++ b/etc/abbrevs	Wed Dec 30 14:05:51 2015 +0100
@@ -3,6 +3,8 @@
 (*prevent replacement of very long arrows*)
 "===>" = "===>"
 
+"--->" = "\<midarrow>\<rightarrow>"
+
 (*HOL-NSA*)
 "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
 "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Deriv.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -148,12 +148,12 @@
   by (simp add: has_derivative_at_within divide_inverse ac_simps)
 
 lemma has_derivative_at:
-  "(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)"
+  "(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)"
   unfolding has_derivative_iff_norm LIM_offset_zero_iff[of _ _ x] by simp
 
 lemma field_has_derivative_at:
   fixes x :: "'a::real_normed_field"
-  shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+  shows "(f has_derivative op * D) (at x) \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   apply (unfold has_derivative_at)
   apply (simp add: bounded_linear_mult_right)
   apply (simp cong: LIM_cong add: nonzero_norm_divide [symmetric])
@@ -454,7 +454,7 @@
   interpret F: bounded_linear F
     using assms by (rule has_derivative_bounded_linear)
   let ?r = "\<lambda>h. norm (F h) / norm h"
-  have *: "?r -- 0 --> 0"
+  have *: "?r \<midarrow>0\<rightarrow> 0"
     using assms unfolding has_derivative_at by simp
   show "F = (\<lambda>h. 0)"
   proof
@@ -599,7 +599,7 @@
 lemma differentiableI: "(f has_real_derivative D) (at x within s) \<Longrightarrow> f differentiable (at x within s)"
   by (force simp add: real_differentiable_def)
 
-lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+lemma DERIV_def: "DERIV f x :> D \<longleftrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right LIM_zero_iff[symmetric, of _ D])
   apply (subst (2) tendsto_norm_zero_iff[symmetric])
   apply (rule filterlim_cong)
@@ -701,7 +701,7 @@
 
 subsection \<open>Derivatives\<close>
 
-lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) -- 0 --> D"
+lemma DERIV_D: "DERIV f x :> D \<Longrightarrow> (\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow> D"
   by (simp add: DERIV_def)
 
 lemma DERIV_const [simp, derivative_intros]: "((\<lambda>x. k) has_field_derivative 0) F"
@@ -883,8 +883,8 @@
 
 lemma DERIV_LIM_iff:
   fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" shows
-     "((%h. (f(a + h) - f(a)) / h) -- 0 --> D) =
-      ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)"
+     "((%h. (f(a + h) - f(a)) / h) \<midarrow>0\<rightarrow> D) =
+      ((%x. (f(x)-f(a)) / (x-a)) \<midarrow>a\<rightarrow> D)"
 apply (rule iffI)
 apply (drule_tac k="- a" in LIM_offset)
 apply simp
@@ -892,7 +892,7 @@
 apply (simp add: add.commute)
 done
 
-lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) --x --> D"
+lemma DERIV_iff2: "(DERIV f x :> D) \<longleftrightarrow> (\<lambda>z. (f z - f x) / (z - x)) \<midarrow>x\<rightarrow> D"
   by (simp add: DERIV_def DERIV_LIM_iff)
 
 lemma DERIV_cong_ev: "x = y \<Longrightarrow> eventually (\<lambda>x. f x = g x) (nhds x) \<Longrightarrow> u = v \<Longrightarrow>
@@ -1485,9 +1485,9 @@
         inverse ((f (g y) - x) / (g y - g x))"
     by (simp add: inj)
 next
-  have "(\<lambda>z. (f z - f (g x)) / (z - g x)) -- g x --> D"
+  have "(\<lambda>z. (f z - f (g x)) / (z - g x)) \<midarrow>g x\<rightarrow> D"
     by (rule der [unfolded DERIV_iff2])
-  hence 1: "(\<lambda>z. (f z - x) / (z - g x)) -- g x --> D"
+  hence 1: "(\<lambda>z. (f z - x) / (z - g x)) \<midarrow>g x\<rightarrow> D"
     using inj a b by simp
   have 2: "\<exists>d>0. \<forall>y. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow> g y \<noteq> g x"
   proof (rule exI, safe)
@@ -1504,10 +1504,10 @@
     also assume "y \<noteq> x"
     finally show False by simp
   qed
-  have "(\<lambda>y. (f (g y) - x) / (g y - g x)) -- x --> D"
+  have "(\<lambda>y. (f (g y) - x) / (g y - g x)) \<midarrow>x\<rightarrow> D"
     using cont 1 2 by (rule isCont_LIM_compose2)
   thus "(\<lambda>y. inverse ((f (g y) - x) / (g y - g x)))
-        -- x --> inverse D"
+        \<midarrow>x\<rightarrow> inverse D"
     using neq by (rule tendsto_inverse)
 qed
 
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -3596,7 +3596,7 @@
   unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
   using lim_ereal by (simp_all add: comp_def)
 
-lemma inverse_infty_ereal_tendsto_0: "inverse -- \<infinity> --> (0::ereal)"
+lemma inverse_infty_ereal_tendsto_0: "inverse \<midarrow>\<infinity>\<rightarrow> (0::ereal)"
 proof -
   have **: "((\<lambda>x. ereal (inverse x)) \<longlongrightarrow> ereal 0) at_infinity"
     by (intro tendsto_intros tendsto_inverse_0)
@@ -3609,10 +3609,10 @@
 
 lemma inverse_ereal_tendsto_pos:
   fixes x :: ereal assumes "0 < x"
-  shows "inverse -- x --> inverse x"
+  shows "inverse \<midarrow>x\<rightarrow> inverse x"
 proof (cases x)
   case (real r)
-  with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) -- r --> ereal (inverse r)"
+  with \<open>0 < x\<close> have **: "(\<lambda>x. ereal (inverse x)) \<midarrow>r\<rightarrow> ereal (inverse r)"
     by (auto intro!: tendsto_inverse)
   from real \<open>0 < x\<close> show ?thesis
     by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Limits.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -1941,40 +1941,40 @@
 
 lemma LIM_eq:
   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
-  shows "f -- a --> L =
+  shows "f \<midarrow>a\<rightarrow> L =
      (\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)"
 by (simp add: LIM_def dist_norm)
 
 lemma LIM_I:
   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
   shows "(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r)
-      ==> f -- a --> L"
+      ==> f \<midarrow>a\<rightarrow> L"
 by (simp add: LIM_eq)
 
 lemma LIM_D:
   fixes a :: "'a::real_normed_vector" and L :: "'b::real_normed_vector"
-  shows "[| f -- a --> L; 0<r |]
+  shows "[| f \<midarrow>a\<rightarrow> L; 0<r |]
       ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (x-a) < s --> norm (f x - L) < r"
 by (simp add: LIM_eq)
 
 lemma LIM_offset:
   fixes a :: "'a::real_normed_vector"
-  shows "f -- a --> L \<Longrightarrow> (\<lambda>x. f (x + k)) -- a - k --> L"
+  shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>x. f (x + k)) \<midarrow>(a - k)\<rightarrow> L"
   unfolding filtermap_at_shift[symmetric, of a k] filterlim_def filtermap_filtermap by simp
 
 lemma LIM_offset_zero:
   fixes a :: "'a::real_normed_vector"
-  shows "f -- a --> L \<Longrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+  shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L"
 by (drule_tac k="a" in LIM_offset, simp add: add.commute)
 
 lemma LIM_offset_zero_cancel:
   fixes a :: "'a::real_normed_vector"
-  shows "(\<lambda>h. f (a + h)) -- 0 --> L \<Longrightarrow> f -- a --> L"
+  shows "(\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L \<Longrightarrow> f \<midarrow>a\<rightarrow> L"
 by (drule_tac k="- a" in LIM_offset, simp)
 
 lemma LIM_offset_zero_iff:
   fixes f :: "'a :: real_normed_vector \<Rightarrow> _"
-  shows  "f -- a --> L \<longleftrightarrow> (\<lambda>h. f (a + h)) -- 0 --> L"
+  shows  "f \<midarrow>a\<rightarrow> L \<longleftrightarrow> (\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> L"
   using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
 
 lemma LIM_zero:
@@ -1995,9 +1995,9 @@
 lemma LIM_imp_LIM:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
   fixes g :: "'a::topological_space \<Rightarrow> 'c::real_normed_vector"
-  assumes f: "f -- a --> l"
+  assumes f: "f \<midarrow>a\<rightarrow> l"
   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> norm (g x - m) \<le> norm (f x - l)"
-  shows "g -- a --> m"
+  shows "g \<midarrow>a\<rightarrow> m"
   by (rule metric_LIM_imp_LIM [OF f],
     simp add: dist_norm le)
 
@@ -2005,23 +2005,23 @@
   fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
   assumes 1: "0 < R"
   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < R\<rbrakk> \<Longrightarrow> f x = g x"
-  shows "g -- a --> l \<Longrightarrow> f -- a --> l"
+  shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>a\<rightarrow> l"
 by (rule metric_LIM_equal2 [OF 1 2], simp_all add: dist_norm)
 
 lemma LIM_compose2:
   fixes a :: "'a::real_normed_vector"
-  assumes f: "f -- a --> b"
-  assumes g: "g -- b --> c"
+  assumes f: "f \<midarrow>a\<rightarrow> b"
+  assumes g: "g \<midarrow>b\<rightarrow> c"
   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> b"
-  shows "(\<lambda>x. g (f x)) -- a --> c"
+  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
 by (rule metric_LIM_compose2 [OF f g inj [folded dist_norm]])
 
 lemma real_LIM_sandwich_zero:
   fixes f g :: "'a::topological_space \<Rightarrow> real"
-  assumes f: "f -- a --> 0"
+  assumes f: "f \<midarrow>a\<rightarrow> 0"
   assumes 1: "\<And>x. x \<noteq> a \<Longrightarrow> 0 \<le> g x"
   assumes 2: "\<And>x. x \<noteq> a \<Longrightarrow> g x \<le> f x"
-  shows "g -- a --> 0"
+  shows "g \<midarrow>a\<rightarrow> 0"
 proof (rule LIM_imp_LIM [OF f]) (* FIXME: use tendsto_sandwich *)
   fix x assume x: "x \<noteq> a"
   have "norm (g x - 0) = g x" by (simp add: 1 x)
@@ -2036,20 +2036,20 @@
 
 lemma LIM_isCont_iff:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
-  shows "(f -- a --> f a) = ((\<lambda>h. f (a + h)) -- 0 --> f a)"
+  shows "(f \<midarrow>a\<rightarrow> f a) = ((\<lambda>h. f (a + h)) \<midarrow>0\<rightarrow> f a)"
 by (rule iffI [OF LIM_offset_zero LIM_offset_zero_cancel])
 
 lemma isCont_iff:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::topological_space"
-  shows "isCont f x = (\<lambda>h. f (x + h)) -- 0 --> f x"
+  shows "isCont f x = (\<lambda>h. f (x + h)) \<midarrow>0\<rightarrow> f x"
 by (simp add: isCont_def LIM_isCont_iff)
 
 lemma isCont_LIM_compose2:
   fixes a :: "'a::real_normed_vector"
   assumes f [unfolded isCont_def]: "isCont f a"
-  assumes g: "g -- f a --> l"
+  assumes g: "g \<midarrow>f a\<rightarrow> l"
   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < d \<longrightarrow> f x \<noteq> f a"
-  shows "(\<lambda>x. g (f x)) -- a --> l"
+  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> l"
 by (rule LIM_compose2 [OF f g inj])
 
 
@@ -2403,7 +2403,7 @@
 text\<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110\<close>
 lemma LIM_fun_gt_zero:
   fixes f :: "real \<Rightarrow> real"
-  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)"
+  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)"
 apply (drule (1) LIM_D, clarify)
 apply (rule_tac x = s in exI)
 apply (simp add: abs_less_iff)
@@ -2411,7 +2411,7 @@
 
 lemma LIM_fun_less_zero:
   fixes f :: "real \<Rightarrow> real"
-  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)"
+  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)"
 apply (drule LIM_D [where r="-l"], simp, clarify)
 apply (rule_tac x = s in exI)
 apply (simp add: abs_less_iff)
@@ -2419,7 +2419,7 @@
 
 lemma LIM_fun_not_zero:
   fixes f :: "real \<Rightarrow> real"
-  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)"
+  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)"
   using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
 
 end
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -2552,7 +2552,7 @@
     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"
       using dpos by blast
   }
-  then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) -- x --> 0"
+  then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \<midarrow>x\<rightarrow> 0"
     by (simp add: Lim_at dist_norm inverse_eq_divide)
   show ?thesis
     apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
@@ -5472,7 +5472,7 @@
   show "(\<lambda>u. f' u / (u - w) ^ (Suc k)) contour_integrable_on \<gamma>"
     by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
   have *: "(\<lambda>n. contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - n) ^ k - inverse (x - w) ^ k) / (n - w) / k))
-           --w--> contour_integral \<gamma> (\<lambda>u. f' u / (u - w) ^ (Suc k))"
+           \<midarrow>w\<rightarrow> contour_integral \<gamma> (\<lambda>u. f' u / (u - w) ^ (Suc k))"
     by (rule contour_integral_uniform_limit [OF 1 2 leB \<gamma>]) auto
   have **: "contour_integral \<gamma> (\<lambda>x. f' x * (inverse (x - u) ^ k - inverse (x - w) ^ k) / ((u - w) * k)) =
               (f u - f w) / (u - w) / k"
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/NSA/CLim.thy
--- a/src/HOL/NSA/CLim.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/NSA/CLim.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -47,22 +47,22 @@
 (** get this result easily now **)
 lemma LIM_Re:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
+  shows "f \<midarrow>a\<rightarrow> L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L)"
 by (simp add: LIM_NSLIM_iff NSLIM_Re)
 
 lemma LIM_Im:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
+  shows "f \<midarrow>a\<rightarrow> L ==> (%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L)"
 by (simp add: LIM_NSLIM_iff NSLIM_Im)
 
 lemma LIM_cnj:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
+  shows "f \<midarrow>a\<rightarrow> L ==> (%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L"
 by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
 
 lemma LIM_cnj_iff:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
+  shows "((%x. cnj (f x)) \<midarrow>a\<rightarrow> cnj L) = (f \<midarrow>a\<rightarrow> L)"
 by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
 
 lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
@@ -84,7 +84,7 @@
 (** much, much easier standard proof **)
 lemma CLIM_CRLIM_iff:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
+  shows "(f \<midarrow>x\<rightarrow> L) = ((%y. cmod(f y - L)) \<midarrow>x\<rightarrow> 0)"
 by (simp add: LIM_eq)
 
 (* so this is nicer nonstandard proof *)
@@ -103,8 +103,8 @@
 
 lemma LIM_CRLIM_Re_Im_iff:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
-  shows "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
-                         (%x. Im(f x)) -- a --> Im(L))"
+  shows "(f \<midarrow>a\<rightarrow> L) = ((%x. Re(f x)) \<midarrow>a\<rightarrow> Re(L) &
+                         (%x. Im(f x)) \<midarrow>a\<rightarrow> Im(L))"
 by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
 
 
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/NSA/HLim.thy
--- a/src/HOL/NSA/HLim.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/NSA/HLim.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -136,7 +136,7 @@
 subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close>
 
 lemma LIM_NSLIM:
-  assumes f: "f -- a --> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
+  assumes f: "f \<midarrow>a\<rightarrow> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
 proof (rule NSLIM_I)
   fix x
   assume neq: "x \<noteq> star_of a"
@@ -164,7 +164,7 @@
 qed
 
 lemma NSLIM_LIM:
-  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f -- a --> L"
+  assumes f: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L" shows "f \<midarrow>a\<rightarrow> L"
 proof (rule LIM_I)
   fix r::real assume r: "0 < r"
   have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
@@ -190,7 +190,7 @@
     by transfer
 qed
 
-theorem LIM_NSLIM_iff: "(f -- x --> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
+theorem LIM_NSLIM_iff: "(f \<midarrow>x\<rightarrow> L) = (f \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S L)"
 by (blast intro: LIM_NSLIM NSLIM_LIM)
 
 
@@ -215,7 +215,7 @@
 
 text\<open>Hence, NS continuity can be given
   in terms of standard limit\<close>
-lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
+lemma isNSCont_LIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow> (f a))"
 by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
 
 text\<open>Moreover, it's trivial now that NS continuity
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -1727,31 +1727,31 @@
 
 subsubsection \<open>Limits of Functions\<close>
 
-lemma LIM_def: "f -- (a::'a::metric_space) --> (L::'b::metric_space) =
+lemma LIM_def: "f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space) =
      (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & dist x a < s
         --> dist (f x) L < r)"
   unfolding tendsto_iff eventually_at by simp
 
 lemma metric_LIM_I:
   "(\<And>r. 0 < r \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r)
-    \<Longrightarrow> f -- (a::'a::metric_space) --> (L::'b::metric_space)"
+    \<Longrightarrow> f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space)"
 by (simp add: LIM_def)
 
 lemma metric_LIM_D:
-  "\<lbrakk>f -- (a::'a::metric_space) --> (L::'b::metric_space); 0 < r\<rbrakk>
+  "\<lbrakk>f \<midarrow>(a::'a::metric_space)\<rightarrow> (L::'b::metric_space); 0 < r\<rbrakk>
     \<Longrightarrow> \<exists>s>0. \<forall>x. x \<noteq> a \<and> dist x a < s \<longrightarrow> dist (f x) L < r"
 by (simp add: LIM_def)
 
 lemma metric_LIM_imp_LIM:
-  assumes f: "f -- a --> (l::'a::metric_space)"
+  assumes f: "f \<midarrow>a\<rightarrow> (l::'a::metric_space)"
   assumes le: "\<And>x. x \<noteq> a \<Longrightarrow> dist (g x) m \<le> dist (f x) l"
-  shows "g -- a --> (m::'b::metric_space)"
+  shows "g \<midarrow>a\<rightarrow> (m::'b::metric_space)"
   by (rule metric_tendsto_imp_tendsto [OF f]) (auto simp add: eventually_at_topological le)
 
 lemma metric_LIM_equal2:
   assumes 1: "0 < R"
   assumes 2: "\<And>x. \<lbrakk>x \<noteq> a; dist x a < R\<rbrakk> \<Longrightarrow> f x = g x"
-  shows "g -- a --> l \<Longrightarrow> f -- (a::'a::metric_space) --> l"
+  shows "g \<midarrow>a\<rightarrow> l \<Longrightarrow> f \<midarrow>(a::'a::metric_space)\<rightarrow> l"
 apply (rule topological_tendstoI)
 apply (drule (2) topological_tendstoD)
 apply (simp add: eventually_at, safe)
@@ -1761,19 +1761,19 @@
 done
 
 lemma metric_LIM_compose2:
-  assumes f: "f -- (a::'a::metric_space) --> b"
-  assumes g: "g -- b --> c"
+  assumes f: "f \<midarrow>(a::'a::metric_space)\<rightarrow> b"
+  assumes g: "g \<midarrow>b\<rightarrow> c"
   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> b"
-  shows "(\<lambda>x. g (f x)) -- a --> c"
+  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
   using inj
   by (intro tendsto_compose_eventually[OF g f]) (auto simp: eventually_at)
 
 lemma metric_isCont_LIM_compose2:
   fixes f :: "'a :: metric_space \<Rightarrow> _"
   assumes f [unfolded isCont_def]: "isCont f a"
-  assumes g: "g -- f a --> l"
+  assumes g: "g \<midarrow>f a\<rightarrow> l"
   assumes inj: "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<noteq> f a"
-  shows "(\<lambda>x. g (f x)) -- a --> l"
+  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> l"
 by (rule metric_LIM_compose2 [OF f g inj])
 
 subsection \<open>Complete metric spaces\<close>
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -1204,16 +1204,16 @@
 
 abbreviation
   LIM :: "('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
-        ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
-  "f -- a --> L \<equiv> (f \<longlongrightarrow> L) (at a)"
+        ("((_)/ \<midarrow>(_)/\<rightarrow> (_))" [60, 0, 60] 60) where
+  "f \<midarrow>a\<rightarrow> L \<equiv> (f \<longlongrightarrow> L) (at a)"
 
-lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
+lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<midarrow>a\<rightarrow> l)"
   unfolding tendsto_def by (simp add: at_within_open[where S=S])
 
 lemma LIM_const_not_eq[tendsto_intros]:
   fixes a :: "'a::perfect_space"
   fixes k L :: "'b::t2_space"
-  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
+  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) \<midarrow>a\<rightarrow> L"
   by (simp add: tendsto_const_iff)
 
 lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
@@ -1221,46 +1221,46 @@
 lemma LIM_const_eq:
   fixes a :: "'a::perfect_space"
   fixes k L :: "'b::t2_space"
-  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
+  shows "(\<lambda>x. k) \<midarrow>a\<rightarrow> L \<Longrightarrow> k = L"
   by (simp add: tendsto_const_iff)
 
 lemma LIM_unique:
   fixes a :: "'a::perfect_space" and L M :: "'b::t2_space"
-  shows "f -- a --> L \<Longrightarrow> f -- a --> M \<Longrightarrow> L = M"
+  shows "f \<midarrow>a\<rightarrow> L \<Longrightarrow> f \<midarrow>a\<rightarrow> M \<Longrightarrow> L = M"
   using at_neq_bot by (rule tendsto_unique)
 
 text \<open>Limits are equal for functions equal except at limit point\<close>
 
-lemma LIM_equal: "\<forall>x. x \<noteq> a --> (f x = g x) \<Longrightarrow> (f -- a --> l) \<longleftrightarrow> (g -- a --> l)"
+lemma LIM_equal: "\<forall>x. x \<noteq> a --> (f x = g x) \<Longrightarrow> (f \<midarrow>a\<rightarrow> l) \<longleftrightarrow> (g \<midarrow>a\<rightarrow> l)"
   unfolding tendsto_def eventually_at_topological by simp
 
-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)"
+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)"
   by (simp add: LIM_equal)
 
-lemma LIM_cong_limit: "f -- x --> L \<Longrightarrow> K = L \<Longrightarrow> f -- x --> K"
+lemma LIM_cong_limit: "f \<midarrow>x\<rightarrow> L \<Longrightarrow> K = L \<Longrightarrow> f \<midarrow>x\<rightarrow> K"
   by simp
 
 lemma tendsto_at_iff_tendsto_nhds:
-  "g -- l --> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
+  "g \<midarrow>l\<rightarrow> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
   unfolding tendsto_def eventually_at_filter
   by (intro ext all_cong imp_cong) (auto elim!: eventually_mono)
 
 lemma tendsto_compose:
-  "g -- l --> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
+  "g \<midarrow>l\<rightarrow> g l \<Longrightarrow> (f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. g (f x)) \<longlongrightarrow> g l) F"
   unfolding tendsto_at_iff_tendsto_nhds by (rule filterlim_compose[of g])
 
-lemma LIM_o: "\<lbrakk>g -- l --> g l; f -- a --> l\<rbrakk> \<Longrightarrow> (g \<circ> f) -- a --> g l"
+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"
   unfolding o_def by (rule tendsto_compose)
 
 lemma tendsto_compose_eventually:
-  "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"
+  "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"
   by (rule filterlim_compose[of g _ "at l"]) (auto simp add: filterlim_at)
 
 lemma LIM_compose_eventually:
-  assumes f: "f -- a --> b"
-  assumes g: "g -- b --> c"
+  assumes f: "f \<midarrow>a\<rightarrow> b"
+  assumes g: "g \<midarrow>b\<rightarrow> c"
   assumes inj: "eventually (\<lambda>x. f x \<noteq> b) (at a)"
-  shows "(\<lambda>x. g (f x)) -- a --> c"
+  shows "(\<lambda>x. g (f x)) \<midarrow>a\<rightarrow> c"
   using g f inj by (rule tendsto_compose_eventually)
 
 lemma tendsto_compose_filtermap: "((g \<circ> f) \<longlongrightarrow> T) F \<longleftrightarrow> (g \<longlongrightarrow> T) (filtermap f F)"
@@ -1280,19 +1280,19 @@
 
 lemma LIMSEQ_SEQ_conv1:
   fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
-  assumes f: "f -- a --> l"
+  assumes f: "f \<midarrow>a\<rightarrow> l"
   shows "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
   using tendsto_compose_eventually [OF f, where F=sequentially] by simp
 
 lemma LIMSEQ_SEQ_conv2:
   fixes f :: "'a::first_countable_topology \<Rightarrow> 'b::topological_space"
   assumes "\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. f (S n)) \<longlonglongrightarrow> l"
-  shows "f -- a --> l"
+  shows "f \<midarrow>a\<rightarrow> l"
   using assms unfolding tendsto_def [where l=l] by (simp add: sequentially_imp_eventually_at)
 
 lemma LIMSEQ_SEQ_conv:
   "(\<forall>S. (\<forall>n. S n \<noteq> a) \<and> S \<longlonglongrightarrow> (a::'a::first_countable_topology) \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L) =
-   (X -- a --> (L::'b::topological_space))"
+   (X \<midarrow>a\<rightarrow> (L::'b::topological_space))"
   using LIMSEQ_SEQ_conv2 LIMSEQ_SEQ_conv1 ..
 
 lemma sequentially_imp_eventually_at_left:
@@ -1585,7 +1585,7 @@
   continuous (at x within s) (\<lambda>x. g (f x))"
   using continuous_within_compose[of x s f g] by (simp add: comp_def)
 
-lemma continuous_at: "continuous (at x) f \<longleftrightarrow> f -- x --> f x"
+lemma continuous_at: "continuous (at x) f \<longleftrightarrow> f \<midarrow>x\<rightarrow> f x"
   using continuous_within[of x UNIV f] by simp
 
 lemma continuous_ident[continuous_intros, simp]: "continuous (at x within S) (\<lambda>x. x)"
@@ -1601,7 +1601,7 @@
 abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool" where
   "isCont f a \<equiv> continuous (at a) f"
 
-lemma isCont_def: "isCont f a \<longleftrightarrow> f -- a --> f a"
+lemma isCont_def: "isCont f a \<longleftrightarrow> f \<midarrow>a\<rightarrow> f a"
   by (rule continuous_at)
 
 lemma continuous_at_imp_continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
diff -r b4b11391c676 -r 3a27957ac658 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Dec 30 11:37:29 2015 +0100
+++ b/src/HOL/Transcendental.thy	Wed Dec 30 14:05:51 2015 +0100
@@ -564,19 +564,19 @@
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes k: "0 < (k::real)"
     and le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
-  shows "f -- 0 --> 0"
+  shows "f \<midarrow>0\<rightarrow> 0"
 proof (rule tendsto_norm_zero_cancel)
-  show "(\<lambda>h. norm (f h)) -- 0 --> 0"
+  show "(\<lambda>h. norm (f h)) \<midarrow>0\<rightarrow> 0"
   proof (rule real_tendsto_sandwich)
     show "eventually (\<lambda>h. 0 \<le> norm (f h)) (at 0)"
       by simp
     show "eventually (\<lambda>h. norm (f h) \<le> K * norm h) (at 0)"
       using k by (auto simp add: eventually_at dist_norm le)
-    show "(\<lambda>h. 0) -- (0::'a) --> (0::real)"
+    show "(\<lambda>h. 0) \<midarrow>(0::'a)\<rightarrow> (0::real)"
       by (rule tendsto_const)
-    have "(\<lambda>h. K * norm h) -- (0::'a) --> K * norm (0::'a)"
+    have "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> K * norm (0::'a)"
       by (intro tendsto_intros)
-    then show "(\<lambda>h. K * norm h) -- (0::'a) --> 0"
+    then show "(\<lambda>h. K * norm h) \<midarrow>(0::'a)\<rightarrow> 0"
       by simp
   qed
 qed
@@ -586,7 +586,7 @@
   assumes k: "0 < (k::real)"
   assumes f: "summable f"
   assumes le: "\<And>h n. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (g h n) \<le> f n * norm h"
-  shows "(\<lambda>h. suminf (g h)) -- 0 --> 0"
+  shows "(\<lambda>h. suminf (g h)) \<midarrow>0\<rightarrow> 0"
 proof (rule lemma_termdiff4 [OF k])
   fix h::'a
   assume "h \<noteq> 0" and "norm h < k"
@@ -615,7 +615,7 @@
   assumes 1: "summable (\<lambda>n. diffs (diffs c) n * K ^ n)"
     and 2: "norm x < norm K"
   shows "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h
-             - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
+             - of_nat n * x ^ (n - Suc 0))) \<midarrow>0\<rightarrow> 0"
 proof -
   from dense [OF 2]
   obtain r where r1: "norm x < r" and r2: "r < norm K" by fast
@@ -682,7 +682,7 @@
   unfolding DERIV_def
 proof (rule LIM_zero_cancel)
   show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x^n)) / h
-            - suminf (\<lambda>n. diffs c n * x^n)) -- 0 --> 0"
+            - suminf (\<lambda>n. diffs c n * x^n)) \<midarrow>0\<rightarrow> 0"
   proof (rule LIM_equal2)
     show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
   next
@@ -702,7 +702,7 @@
           (\<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0)))"
       by (simp add: algebra_simps)
   next
-    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) -- 0 --> 0"
+    show "(\<lambda>h. \<Sum>n. c n * (((x + h) ^ n - x^n) / h - of_nat n * x ^ (n - Suc 0))) \<midarrow>0\<rightarrow> 0"
       by (rule termdiffs_aux [OF 3 4])
   qed
 qed
@@ -4068,7 +4068,7 @@
   "continuous (at x within s) f \<Longrightarrow> cos (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. tan (f x))"
   unfolding continuous_within by (rule tendsto_tan)
 
-lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) -- pi/2 --> 0"
+lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) \<midarrow>pi/2\<rightarrow> 0"
   by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
 
 lemma lemma_tan_total: "0 < y ==> \<exists>x. 0 < x & x < pi/2 & y < tan x"
@@ -5572,7 +5572,7 @@
   }
   then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
     using Suc  by auto
-  then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
+  then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) \<midarrow>0\<rightarrow> 0"
     by (simp cong: LIM_cong)                   \<comment>\<open>the case @{term"w=0"} by continuity\<close>
   then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
     using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique