--- a/src/HOL/Probability/Sigma_Algebra.thy Wed Dec 01 19:42:09 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Wed Dec 01 20:09:41 2010 +0100
@@ -397,6 +397,12 @@
by (auto intro: sigma_sets.Empty sigma_sets_top)
qed
+lemma (in sigma_algebra) sets_sigma_subset:
+ assumes "space N = space M"
+ assumes "sets N \<subseteq> sets M"
+ shows "sets (sigma N) \<subseteq> sets M"
+ by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms)
+
section {* Measurable functions *}
definition
@@ -1149,7 +1155,6 @@
section {* Dynkin systems *}
-
locale dynkin_system =
fixes M :: "'a algebra"
assumes space_closed: "sets M \<subseteq> Pow (space M)"