src/HOL/Analysis/Harmonic_Numbers.thy

   and the Euler-Mascheroni constant.
 \<close>
 
 subsection \<open>The Harmonic numbers\<close>
 
-definition%important harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
+definition\<^marker>\<open>tag important\<close> harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
   "harm n = (\<Sum>k=1..n. inverse (of_nat k))"
 
 lemma harm_altdef: "harm n = (\<Sum>k<n. inverse (of_nat (Suc k)))"
   unfolding harm_def by (induction n) simp_all
 

   have "convergent (\<lambda>n. harm (Suc n) - ln (of_nat (Suc n) :: real))"
     by (subst A) (fact euler_mascheroni.sum_integral_diff_series_convergent)
   thus ?thesis by (subst (asm) convergent_Suc_iff)
 qed
 
-lemma%important euler_mascheroni_LIMSEQ:
+lemma\<^marker>\<open>tag important\<close> euler_mascheroni_LIMSEQ:
   "(\<lambda>n. harm n - ln (of_nat n) :: real) \<longlonglongrightarrow> euler_mascheroni"
   unfolding euler_mascheroni_def
   by (simp add: convergent_LIMSEQ_iff [symmetric] euler_mascheroni_convergent)
 
 lemma euler_mascheroni_LIMSEQ_of_real:

       by (induction n) (simp_all add: inverse_eq_divide)
   qed
 qed
 
 
-subsection%unimportant \<open>Bounds on the Euler-Mascheroni constant\<close>
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Bounds on the Euler-Mascheroni constant\<close>
 
 (* TODO: Move? *)
 lemma ln_inverse_approx_le:
   assumes "(x::real) > 0" "a > 0"
   shows   "ln (x + a) - ln x \<le> a * (inverse x + inverse (x + a))/2" (is "_ \<le> ?A")