src/HOL/Multivariate_Analysis/Derivative.thy

           show ?case unfolding dist_norm using N[rule_format,OF goal1 `x\<in>s`, of u] False `e>0`
             by (auto simp add:field_simps) qed qed qed
     show "bounded_linear (g' x)" unfolding linear_linear linear_def apply(rule,rule,rule) defer proof(rule,rule)
       fix x' y z::"'m" and c::real
       note lin = assms(2)[rule_format,OF `x\<in>s`,THEN derivative_linear]
-      show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" apply(rule Lim_unique[OF trivial_limit_sequentially])
+      show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" apply(rule tendsto_unique[OF trivial_limit_sequentially])
         apply(rule lem3[rule_format])
         unfolding lin[unfolded bounded_linear_def bounded_linear_axioms_def,THEN conjunct2,THEN conjunct1,rule_format]
         apply(rule Lim_cmul) by(rule lem3[rule_format])
-      show "g' x (y + z) = g' x y + g' x z" apply(rule Lim_unique[OF trivial_limit_sequentially])
+      show "g' x (y + z) = g' x y + g' x z" apply(rule tendsto_unique[OF trivial_limit_sequentially])
         apply(rule lem3[rule_format]) unfolding lin[unfolded bounded_linear_def additive_def,THEN conjunct1,rule_format]
         apply(rule Lim_add) by(rule lem3[rule_format])+ qed 
     show "\<forall>e>0. \<exists>d>0. \<forall>y\<in>s. norm (y - x) < d \<longrightarrow> norm (g y - g x - g' x (y - x)) \<le> e * norm (y - x)" proof(rule,rule) case goal1
       have *:"e/3>0" using goal1 by auto guess N1 using assms(3)[rule_format,OF *] .. note N1=this
       guess N2 using lem2[rule_format,OF *] .. note N2=this