# HG changeset patch
# User paulson
# Date 1256732498 0
# Node ID 9290fbf0a30e9a33afacd48535bf76bbbd0e7e2d
# Parent  73a0c804840fbe5ebbbf12a35d4cc7e5fc005636
Probability tweaks

diff -r 73a0c804840f -r 9290fbf0a30e NEWS
--- 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;
diff -r 73a0c804840f -r 9290fbf0a30e src/HOL/Probability/Measure.thy
--- 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)"