--- a/NEWS Wed Oct 28 11:43:06 2009 +0000
+++ b/NEWS Wed Oct 28 12:21:38 2009 +0000
@@ -67,7 +67,7 @@
* New theory SupInf of the supremum and infimum operators for sets of reals.
-* New theory Probability containing a development of measure theory, eventually leading to Lebesgue integration and probability.
+* New theory Probability, which contains a development of measure theory, eventually leading to Lebesgue integration and probability.
* Split off prime number ingredients from theory GCD
to theory Number_Theory/Primes;
--- a/src/HOL/Probability/Measure.thy Wed Oct 28 11:43:06 2009 +0000
+++ b/src/HOL/Probability/Measure.thy Wed Oct 28 12:21:38 2009 +0000
@@ -823,13 +823,7 @@
lemma (in sigma_algebra) sigma_algebra_extend:
"sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
-proof -
- have 1: "sigma_algebra M \<Longrightarrow> ?thesis"
- by (simp add: sigma_algebra_def algebra_def sigma_algebra_axioms_def)
- show ?thesis
- by (rule 1) intro_locales
-qed
-
+ by unfold_locales (auto intro!: space_closed)
lemma (in sigma_algebra) finite_additivity_sufficient:
assumes fin: "finite (space M)"