| changeset 58876 | 1888e3cb8048 |
| parent 57447 | 87429bdecad5 |
| child 61359 | e985b52c3eb3 |
--- a/src/HOL/Probability/Projective_Family.thy Sun Nov 02 16:59:40 2014 +0100 +++ b/src/HOL/Probability/Projective_Family.thy Sun Nov 02 17:06:05 2014 +0100 @@ -3,7 +3,7 @@ Author: Johannes Hölzl, TU München *) -header {*Projective Family*} +section {*Projective Family*} theory Projective_Family imports Finite_Product_Measure Probability_Measure