src/HOL/Probability/Independent_Family.thy
changeset 58876 1888e3cb8048
parent 57512 cc97b347b301
child 59000 6eb0725503fc
     1.1 --- a/src/HOL/Probability/Independent_Family.thy	Sun Nov 02 16:59:40 2014 +0100
     1.2 +++ b/src/HOL/Probability/Independent_Family.thy	Sun Nov 02 17:06:05 2014 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Sudeep Kanav, TU M√ľnchen
     1.5  *)
     1.6  
     1.7 -header {* Independent families of events, event sets, and random variables *}
     1.8 +section {* Independent families of events, event sets, and random variables *}
     1.9  
    1.10  theory Independent_Family
    1.11    imports Probability_Measure Infinite_Product_Measure