changeset 58876 | 1888e3cb8048 |
parent 58606 | 9c66f7c541fb |
child 59000 | 6eb0725503fc |
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Sun Nov 02 16:59:40 2014 +0100 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Sun Nov 02 17:06:05 2014 +0100 @@ -3,7 +3,7 @@ Author: Armin Heller, TU München *) -header {* Lebesgue Integration for Nonnegative Functions *} +section {* Lebesgue Integration for Nonnegative Functions *} theory Nonnegative_Lebesgue_Integration imports Measure_Space Borel_Space