--- a/src/HOL/Analysis/Finite_Product_Measure.thy Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Fri Jan 25 14:59:40 2019 +0100
@@ -397,7 +397,7 @@
apply (auto intro!: arg_cong2[where f=sigma_sets])
done
-lemma (*FIX ME needs name *)
+lemma
shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)