src/HOL/Analysis/Derivative.thy

     (\<forall>e>0. \<exists>d>0. \<forall>x'. 0 < norm (x' - x) \<and> norm (x' - x) < d \<longrightarrow>
       norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)"
   using has_derivative_within' [of f f' x UNIV]
   by simp
 
-lemma has_derivative_at_within:
+lemma has_derivative_at_withinI:
   "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f') (at x within s)"
   unfolding has_derivative_within' has_derivative_at'
   by blast
 
 lemma has_derivative_within_open:

 lemma differentiable_onD: "\<lbrakk>f differentiable_on S; x \<in> S\<rbrakk> \<Longrightarrow> f differentiable (at x within S)"
   using differentiable_on_def by blast
 
 lemma differentiable_at_withinI: "f differentiable (at x) \<Longrightarrow> f differentiable (at x within s)"
   unfolding differentiable_def
-  using has_derivative_at_within
+  using has_derivative_at_withinI
   by blast
 
 lemma differentiable_at_imp_differentiable_on:
   "(\<And>x. x \<in> s \<Longrightarrow> f differentiable at x) \<Longrightarrow> f differentiable_on s"
   by (metis differentiable_at_withinI differentiable_on_def)

           apply (simp add: comp_def)
           apply (rule bounded_linear.has_derivative[OF assms(3)])
           apply (rule derivative_intros)
           defer
           apply (rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
-          apply (rule has_derivative_at_within)
+          apply (rule has_derivative_at_withinI)
           using assms(5) and \<open>u \<in> s\<close> \<open>a \<in> s\<close>
           apply (auto intro!: derivative_intros bounded_linear.has_derivative[of _ "\<lambda>x. x"] has_derivative_bounded_linear)
           done
         have **: "bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)"
           apply (rule_tac[!] bounded_linear_sub)

   by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
 
 lemma has_vector_derivative_at_within:
   "(f has_vector_derivative f') (at x) \<Longrightarrow> (f has_vector_derivative f') (at x within s)"
   unfolding has_vector_derivative_def
-  by (rule has_derivative_at_within)
+  by (rule has_derivative_at_withinI)
 
 lemma has_vector_derivative_weaken:
   fixes x D and f g s t
   assumes f: "(f has_vector_derivative D) (at x within t)"
     and "x \<in> s" "s \<subseteq> t"