src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy

         using i yx  by (simp add: contour_integral_unique divide_less_eq)
     }
     then have "\<exists>d>0. \<forall>y\<in>s. y \<noteq> x \<and> cmod (y-x) < d \<longrightarrow> cmod (?pathint x y - f x * (y-x)) / cmod (y-x) < e"
       using d1 by blast
   }
-  then have *: "((\<lambda>y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) ---> 0) (at x within s)"
+  then have *: "((\<lambda>y. (contour_integral (linepath x y) f - f x * (y - x)) /\<^sub>R cmod (y - x)) \<longlongrightarrow> 0) (at x within s)"
     by (simp add: Lim_within dist_norm inverse_eq_divide)
   show ?thesis
     apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
     apply (rule Lim_transform [OF * Lim_eventually])
     using linordered_field_no_ub

   assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on \<gamma>) F"
       and ev_no: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> path_image \<gamma>. norm(f n x - l x) < e) F"
       and noleB: "\<And>t. t \<in> {0..1} \<Longrightarrow> norm (vector_derivative \<gamma> (at t)) \<le> B"
       and \<gamma>: "valid_path \<gamma>"
       and [simp]: "~ (trivial_limit F)"
-  shows "l contour_integrable_on \<gamma>" "((\<lambda>n. contour_integral \<gamma> (f n)) ---> contour_integral \<gamma> l) F"
+  shows "l contour_integrable_on \<gamma>" "((\<lambda>n. contour_integral \<gamma> (f n)) \<longlongrightarrow> contour_integral \<gamma> l) F"
 proof -
   have "0 \<le> B" by (meson noleB [of 0] atLeastAtMost_iff norm_ge_zero order_refl order_trans zero_le_one)
   { fix e::real
     assume "0 < e"
     then have eB: "0 < e / (\<bar>B\<bar> + 1)" by simp

       apply (rule le_less_trans [OF integral_norm_bound_integral ie])
       apply (simp add: lintg integrable_diff contour_integrable_on [symmetric])
       apply (blast intro: *)+
       done
   }
-  then show "((\<lambda>n. contour_integral \<gamma> (f n)) ---> contour_integral \<gamma> l) F"
+  then show "((\<lambda>n. contour_integral \<gamma> (f n)) \<longlongrightarrow> contour_integral \<gamma> l) F"
     by (rule tendstoI)
 qed
 
 proposition contour_integral_uniform_limit_circlepath:
   assumes ev_fint: "eventually (\<lambda>n::'a. (f n) contour_integrable_on (circlepath z r)) F"
       and ev_no: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> path_image (circlepath z r). norm(f n x - l x) < e) F"
       and [simp]: "~ (trivial_limit F)" "0 < r"
-  shows "l contour_integrable_on (circlepath z r)" "((\<lambda>n. contour_integral (circlepath z r) (f n)) ---> contour_integral (circlepath z r) l) F"
+  shows "l contour_integrable_on (circlepath z r)" "((\<lambda>n. contour_integral (circlepath z r) (f n)) \<longlongrightarrow> contour_integral (circlepath z r) l) F"
 by (auto simp: vector_derivative_circlepath norm_mult intro: contour_integral_uniform_limit assms)
 
 
 subsection\<open> General stepping result for derivative formulas.\<close>
 

 subsection\<open>The Liouville theorem and the Fundamental Theorem of Algebra.\<close>
 
 text\<open> These weak Liouville versions don't even need the derivative formula.\<close>
 
 lemma Liouville_weak_0: 
-  assumes holf: "f holomorphic_on UNIV" and inf: "(f ---> 0) at_infinity"
+  assumes holf: "f holomorphic_on UNIV" and inf: "(f \<longlongrightarrow> 0) at_infinity"
     shows "f z = 0"
 proof (rule ccontr)
   assume fz: "f z \<noteq> 0"
   with inf [unfolded Lim_at_infinity, rule_format, of "norm(f z)/2"]
   obtain B where B: "\<And>x. B \<le> cmod x \<Longrightarrow> norm (f x) * 2 < cmod (f z)"

     using has_contour_integral_bound_circlepath [OF *, of "norm(f z)/2/R"]
     by (auto simp: norm_mult norm_divide divide_simps)
 qed
 
 proposition Liouville_weak: 
-  assumes "f holomorphic_on UNIV" and "(f ---> l) at_infinity"
+  assumes "f holomorphic_on UNIV" and "(f \<longlongrightarrow> l) at_infinity"
     shows "f z = l"
   using Liouville_weak_0 [of "\<lambda>z. f z - l"]
   by (simp add: assms holomorphic_on_const holomorphic_on_diff LIM_zero)
 
 

     obtains z where "f z = 0"
 proof -
   { assume f: "\<And>z. f z \<noteq> 0"
     have 1: "(\<lambda>x. 1 / f x) holomorphic_on UNIV"
       by (simp add: holomorphic_on_divide holomorphic_on_const assms f)
-    have 2: "((\<lambda>x. 1 / f x) ---> 0) at_infinity"
+    have 2: "((\<lambda>x. 1 / f x) \<longlongrightarrow> 0) at_infinity"
       apply (rule tendstoI [OF eventually_mono])
       apply (rule_tac B="2/e" in unbounded)
       apply (simp add: dist_norm norm_divide divide_simps mult_ac)
       done
     have False

       apply (rule_tac e1="e * d" in eventually_mono [OF lim])
       apply (force simp: dist_norm intro: dle mult_left_mono less_le_trans)+
       done
     have g_cint: "(\<lambda>u. g u/(u - w)) contour_integrable_on circlepath z r"
       by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
-    have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) ---> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
+    have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) \<longlongrightarrow> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
       by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \<open>0 < r\<close>])
-    have f_tends_cig: "((\<lambda>n. 2 * of_real pi * ii * f n w) ---> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
+    have f_tends_cig: "((\<lambda>n. 2 * of_real pi * ii * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
       apply (rule Lim_transform_eventually [where f = "\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. f n u/(u - w))"])
       apply (rule eventually_mono [OF cont])
       apply (rule contour_integral_unique [OF Cauchy_integral_circlepath])
       using w
       apply (auto simp: norm_minus_commute dist_norm cif_tends_cig)
       done
-    have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) ---> 2 * of_real pi * \<i> * g w) F"
+    have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> 2 * of_real pi * \<i> * g w) F"
       apply (rule tendsto_mult_left [OF tendstoI])
       apply (rule eventually_mono [OF lim], assumption)
       using w
       apply (force simp add: dist_norm)
       done

                                (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))) F"
       and lim: "\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>n. \<forall>x \<in> cball z r. norm(f n x - g x) < e) F"
       and F:  "~ trivial_limit F" and "0 < r"
   obtains g' where
       "continuous_on (cball z r) g" 
-      "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) ---> g' w) F"
+      "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F"
 proof -
   let ?conint = "contour_integral (circlepath z r)"
   have g: "continuous_on (cball z r) g" "g holomorphic_on ball z r"
     by (rule holomorphic_uniform_limit [OF eventually_mono [OF cont] lim F]; 
              auto simp: holomorphic_on_open complex_differentiable_def)+
   then obtain g' where g': "\<And>x. x \<in> ball z r \<Longrightarrow> (g has_field_derivative g' x) (at x)"
     using DERIV_deriv_iff_has_field_derivative
     by (fastforce simp add: holomorphic_on_open)
   then have derg: "\<And>x. x \<in> ball z r \<Longrightarrow> deriv g x = g' x"
     by (simp add: DERIV_imp_deriv)
-  have tends_f'n_g': "((\<lambda>n. f' n w) ---> g' w) F" if w: "w \<in> ball z r" for w
+  have tends_f'n_g': "((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F" if w: "w \<in> ball z r" for w
   proof -
     have eq_f': "?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2) = (f' n w - g' w) * (2 * of_real pi * \<i>)" 
              if cont_fn: "continuous_on (cball z r) (f n)" 
              and fnd: "\<And>w. w \<in> ball z r \<Longrightarrow> (f n has_field_derivative f' n w) (at w)" for n
     proof -

       apply (rule eventually_mono [OF lim, of "e*d"])
       apply (simp add: \<open>0 < d\<close>)
       apply (force simp add: dist_norm dle intro: less_le_trans)
       done
     have "((\<lambda>n. contour_integral (circlepath z r) (\<lambda>x. f n x / (x - w)\<^sup>2)) 
-             ---> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
+             \<longlongrightarrow> contour_integral (circlepath z r) ((\<lambda>x. g x / (x - w)\<^sup>2))) F"
       by (rule Cauchy_Integral_Thm.contour_integral_uniform_limit_circlepath [OF 1 2 F \<open>0 < r\<close>])
-    then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) ---> 0) F"
+    then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) \<longlongrightarrow> 0) F"
       using Lim_null by (force intro!: tendsto_mult_right_zero)
-    have "((\<lambda>n. f' n w - g' w) ---> 0) F"
+    have "((\<lambda>n. f' n w - g' w) \<longlongrightarrow> 0) F"
       apply (rule Lim_transform_eventually [OF _ tendsto_0])
       apply (force simp add: divide_simps intro: eq_f' eventually_mono [OF cont])
       done
     then show ?thesis using Lim_null by blast
   qed
-  obtain g' where "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) ---> g' w) F"
+  obtain g' where "\<And>w. w \<in> ball z r \<Longrightarrow> (g has_field_derivative (g' w)) (at w) \<and> ((\<lambda>n. f' n w) \<longlongrightarrow> g' w) F"
       by (blast intro: tends_f'n_g' g' )
   then show ?thesis using g
     using that by blast
 qed