changeset 42067 | 66c8281349ec |
parent 42066 | 6db76c88907a |
child 42866 | b0746bd57a41 |
42066:6db76c88907a | 42067:66c8281349ec |
---|---|
1 (* Author: Lawrence C Paulson; Armin Heller, Johannes Hoelzl, TU Muenchen *) |
1 (* Title: HOL/Probability/Measure.thy |
2 Author: Lawrence C Paulson |
|
3 Author: Johannes Hölzl, TU München |
|
4 Author: Armin Heller, TU München |
|
5 *) |
|
6 |
|
7 header {* Properties about measure spaces *} |
|
2 |
8 |
3 theory Measure |
9 theory Measure |
4 imports Caratheodory |
10 imports Caratheodory |
5 begin |
11 begin |
6 |
12 |