| changeset 42067 | 66c8281349ec |
| parent 41981 | cdf7693bbe08 |
| child 42950 | 6e5c2a3c69da |
| 42066:6db76c88907a | 42067:66c8281349ec |
|---|---|
1 (* Author: Armin Heller, Johannes Hoelzl, TU Muenchen *) |
1 (* Title: HOL/Probability/Lebesgue_Integration.thy |
2 Author: Johannes Hölzl, TU München |
|
3 Author: Armin Heller, TU München |
|
4 *) |
|
2 |
5 |
3 header {*Lebesgue Integration*} |
6 header {*Lebesgue Integration*} |
4 |
7 |
5 theory Lebesgue_Integration |
8 theory Lebesgue_Integration |
6 imports Measure Borel_Space |
9 imports Measure Borel_Space |