--- a/src/HOL/Analysis/Sigma_Algebra.thy Thu Dec 29 22:14:25 2022 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Fri Dec 30 17:48:41 2022 +0000
@@ -1586,7 +1586,7 @@
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: