equal
deleted
inserted
replaced
2 Author: Lawrence C Paulson |
2 Author: Lawrence C Paulson |
3 Author: Johannes Hölzl, TU München |
3 Author: Johannes Hölzl, TU München |
4 Author: Armin Heller, TU München |
4 Author: Armin Heller, TU München |
5 *) |
5 *) |
6 |
6 |
7 section \<open>Measure spaces and their properties\<close> |
7 section \<open>Measure Spaces\<close> |
8 |
8 |
9 theory Measure_Space |
9 theory Measure_Space |
10 imports |
10 imports |
11 Measurable "HOL-Library.Extended_Nonnegative_Real" |
11 Measurable "HOL-Library.Extended_Nonnegative_Real" |
12 begin |
12 begin |