src/HOL/Analysis/Binary_Product_Measure.thy
changeset 69517 dc20f278e8f3
parent 69313 b021008c5397
child 69566 c41954ee87cf
--- 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