--- a/src/HOL/Analysis/Binary_Product_Measure.thy Tue Jan 01 20:57:54 2019 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Tue Jan 01 21:47:27 2019 +0100
@@ -336,7 +336,7 @@
by (simp add: ac_simps)
qed
-subsection%important \<open>Binary products of $\sigma$-finite emeasure spaces\<close>
+subsection%important \<open>Binary products of \<open>\<sigma>\<close>-finite emeasure spaces\<close>
locale%important pair_sigma_finite = M1?: sigma_finite_measure M1 + M2?: sigma_finite_measure M2
for M1 :: "'a measure" and M2 :: "'b measure"