equal
deleted
inserted
replaced
1 (* Title: HOL/Probability/Borel_Space.thy |
1 (* Title: HOL/Probability/Borel_Space.thy |
2 Author: Johannes Hölzl, TU München |
2 Author: Johannes Hölzl, TU München |
3 Author: Armin Heller, TU München |
3 Author: Armin Heller, TU München |
4 *) |
4 *) |
5 |
5 |
6 header {*Borel spaces*} |
6 section {*Borel spaces*} |
7 |
7 |
8 theory Borel_Space |
8 theory Borel_Space |
9 imports |
9 imports |
10 Measurable |
10 Measurable |
11 "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" |
11 "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" |