diff -r 8a17349143df -r ab08604729a2 src/HOL/Analysis/Sigma_Algebra.thy
--- 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: