src/HOL/Analysis/Sigma_Algebra.thy

   with eq show ?thesis
     by (auto simp add: measure_of_def intro!: arg_cong[where f=Abs_measure])
 qed
 
 lemma
-  shows space_measure_of_conv: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
+  shows space_measure_of_conv [simp]: "space (measure_of \<Omega> A \<mu>) = \<Omega>" (is ?space)
   and sets_measure_of_conv:
   "sets (measure_of \<Omega> A \<mu>) = (if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>})" (is ?sets)
   and emeasure_measure_of_conv:
   "emeasure (measure_of \<Omega> A \<mu>) =
   (\<lambda>B. if B \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> B else 0)" (is ?emeasure)