src/HOL/Analysis/Derivative.thy

 lemma has_derivative_add_const:
   "(f has_derivative f') net \<Longrightarrow> ((\<lambda>x. f x + c) has_derivative f') net"
   by (intro derivative_eq_intros) auto
 
 
-subsection%unimportant \<open>Derivative with composed bilinear function\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Derivative with composed bilinear function\<close>
 
 text \<open>More explicit epsilon-delta forms.\<close>
 
 proposition has_derivative_within':
   "(f has_derivative f')(at x within s) \<longleftrightarrow>

     by (auto simp add: continuous_within has_field_derivative_iff cong: Lim_cong_within)
 qed
 
 subsection \<open>Differentiability\<close>
 
-definition%important
+definition\<^marker>\<open>tag important\<close>
   differentiable_on :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a set \<Rightarrow> bool"
     (infix "differentiable'_on" 50)
   where "f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable (at x within s))"
 
 lemma differentiableI: "(f has_derivative f') net \<Longrightarrow> f differentiable net"

 
 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)
 
-corollary%unimportant differentiable_iff_scaleR:
+corollary\<^marker>\<open>tag unimportant\<close> differentiable_iff_scaleR:
   fixes f :: "real \<Rightarrow> 'a::real_normed_vector"
   shows "f differentiable F \<longleftrightarrow> (\<exists>d. (f has_derivative (\<lambda>x. x *\<^sub>R d)) F)"
   by (auto simp: differentiable_def dest: has_derivative_linear linear_imp_scaleR)
 
 lemma differentiable_on_eq_differentiable_at:

   linear.scaleR[OF has_derivative_linear[OF Dg]]
   unfolding has_vector_derivative_def o_def
   by (auto simp: o_def mult.commute has_vector_derivative_def)
 
 
-subsection%unimportant \<open>Composition rules stated just for differentiability\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Composition rules stated just for differentiability\<close>
 
 lemma differentiable_chain_at:
   "f differentiable (at x) \<Longrightarrow>
     g differentiable (at (f x)) \<Longrightarrow> (g \<circ> f) differentiable (at x)"
   unfolding differentiable_def

 
 
 subsection \<open>Uniqueness of derivative\<close>
 
 
-text%important \<open>
+text\<^marker>\<open>tag important\<close> \<open>
  The general result is a bit messy because we need approachability of the
  limit point from any direction. But OK for nontrivial intervals etc.
 \<close>
 
 proposition frechet_derivative_unique_within:

   using assms(2-3) vector_derivative_works
   by auto
 
 subsection \<open>Field differentiability\<close>
 
-definition%important field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
+definition\<^marker>\<open>tag important\<close> field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
            (infixr "(field'_differentiable)" 50)
   where "f field_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
 
 lemma field_differentiable_imp_differentiable:
   "f field_differentiable F \<Longrightarrow> f differentiable F"

   using exp_scaleR_has_vector_derivative_right[of A t]
   by (simp add: exp_times_scaleR_commute)
 
 subsection \<open>Field derivative\<close>
 
-definition%important deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
+definition\<^marker>\<open>tag important\<close> deriv :: "('a \<Rightarrow> 'a::real_normed_field) \<Rightarrow> 'a \<Rightarrow> 'a" where
   "deriv f x \<equiv> SOME D. DERIV f x :> D"
 
 lemma DERIV_imp_deriv: "DERIV f x :> f' \<Longrightarrow> deriv f x = f'"
   unfolding deriv_def by (metis some_equality DERIV_unique)
 

   then show "bounded_linear (\<lambda>(tx, ty). fx tx + blinfun_apply (fy x y) ty)"
     by (auto intro!: bounded_linear_intros simp: split_beta')
 qed
 
 
-subsection%unimportant \<open>Differentiable case distinction\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Differentiable case distinction\<close>
 
 lemma has_derivative_within_If_eq:
   "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within S) =
     (bounded_linear f' \<and>
      ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)