src/HOL/Analysis/Caratheodory.thy

     by (simp add: suminf_eq_SUP)
 qed
 
 subsection \<open>Characterizations of Measures\<close>
 
-definition%important outer_measure_space where
+definition\<^marker>\<open>tag important\<close> outer_measure_space where
   "outer_measure_space M f \<longleftrightarrow> positive M f \<and> increasing M f \<and> countably_subadditive M f"
 
-subsubsection%important \<open>Lambda Systems\<close>
-
-definition%important lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set"
+subsubsection\<^marker>\<open>tag important\<close> \<open>Lambda Systems\<close>
+
+definition\<^marker>\<open>tag important\<close> lambda_system :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set set"
 where
   "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
 
 lemma (in algebra) lambda_system_eq:
   "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}"

   ultimately
   show ?thesis
     using pos by (simp add: measure_space_def)
 qed
 
-definition%important outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set \<Rightarrow> ennreal" where
+definition\<^marker>\<open>tag important\<close> outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set \<Rightarrow> ennreal" where
    "outer_measure M f X =
      (INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"
 
 lemma (in ring_of_sets) outer_measure_agrees:
   assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \<in> M"

   show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
 qed (rule cont)
 
 subsection \<open>Volumes\<close>
 
-definition%important volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
+definition\<^marker>\<open>tag important\<close> volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
   "volume M f \<longleftrightarrow>
   (f {} = 0) \<and> (\<forall>a\<in>M. 0 \<le> f a) \<and>
   (\<forall>C\<subseteq>M. disjoint C \<longrightarrow> finite C \<longrightarrow> \<Union>C \<in> M \<longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c))"
 
 lemma volumeI:

     finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b"
       using Ca Cb by simp
   qed
 qed
 
-subsubsection%important \<open>Caratheodory on semirings\<close>
+subsubsection\<^marker>\<open>tag important\<close> \<open>Caratheodory on semirings\<close>
 
 theorem (in semiring_of_sets) caratheodory:
   assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
   shows "\<exists>\<mu>' :: 'a set \<Rightarrow> ennreal. (\<forall>s \<in> M. \<mu>' s = \<mu> s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>'"
 proof -