diff -r 6db76c88907a -r 66c8281349ec src/HOL/Probability/Product_Measure.thy --- a/src/HOL/Probability/Product_Measure.thy Tue Mar 22 18:53:05 2011 +0100 +++ b/src/HOL/Probability/Product_Measure.thy Tue Mar 22 20:06:10 2011 +0100 @@ -1,3 +1,9 @@ +(* Title: HOL/Probability/Product_Measure.thy + Author: Johannes Hölzl, TU München +*) + +header {*Product measure spaces*} + theory Product_Measure imports Lebesgue_Integration begin