src/HOL/Deriv.thy

   ((\<lambda>x. f x ^ n) has_field_derivative of_nat n * (D * f x ^ (n - Suc 0))) (at x within s)"
   by (rule has_derivative_imp_has_field_derivative[OF has_derivative_power])
      (auto simp: has_field_derivative_def)
 
 lemma DERIV_pow: "((\<lambda>x. x ^ n) has_field_derivative real n * (x ^ (n - Suc 0))) (at x within s)"
-  apply (cut_tac DERIV_power [OF DERIV_ident])
-  apply (simp add: real_of_nat_def)
-  done
+  using DERIV_power [OF DERIV_ident] by simp
 
 lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow> 
   ((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
   using has_derivative_compose[of f "op * D" x s g "op * E"]
   unfolding has_field_derivative_def mult_commute_abs ac_simps .

 lemma DERIV_chain3: (*HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV*)
   assumes "(\<And>x. DERIV g x :> g'(x))"
       and "DERIV f x :> f'" 
     shows "DERIV (\<lambda>x. g(f x)) x :> f' * g'(f x)"
   by (metis UNIV_I DERIV_chain_s [of UNIV] assms)
-
-declare
-  DERIV_power[where 'a=real, unfolded real_of_nat_def[symmetric], derivative_intros]
 
 text\<open>Alternative definition for differentiability\<close>
 
 lemma DERIV_LIM_iff:
   fixes f :: "'a::{real_normed_vector,inverse} \<Rightarrow> 'a" shows