diff -r 09bb8f470959 -r dc20f278e8f3 src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Thu Dec 27 23:38:55 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Dec 28 10:29:59 2018 +0100
@@ -2,7 +2,7 @@
     Author:     Johannes Hölzl, TU München
 *)
 
-section%important \<open>Binary product measures\<close>
+section%important \<open>Binary Product Measure\<close>
 
 theory Binary_Product_Measure
 imports Nonnegative_Lebesgue_Integration