# HG changeset patch
# User hoelzl
# Date 1283450236 -7200
# Node ID 21e9bd6cf0a8bf2b9d0c70a997d9fad6d9b8ed47
# Parent  943c7b348524f0e10916a7780d05cdc5c87c37cf
Corrected definition and hence removed sorry.

diff -r 943c7b348524 -r 21e9bd6cf0a8 src/HOL/Probability/Product_Measure.thy
--- a/src/HOL/Probability/Product_Measure.thy	Thu Sep 02 19:51:53 2010 +0200
+++ b/src/HOL/Probability/Product_Measure.thy	Thu Sep 02 19:57:16 2010 +0200
@@ -5,7 +5,7 @@
 definition "dynkin M \<longleftrightarrow>
   space M \<in> sets M \<and>
   (\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
-  (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
+  (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<subseteq> b \<longrightarrow> b - a \<in> sets M) \<and>
   (\<forall>A. disjoint_family A \<and> range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
 
 lemma dynkinI:
@@ -14,7 +14,7 @@
   assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
           \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
   shows "dynkin M"
-using assms unfolding dynkin_def sorry
+using assms by (auto simp: dynkin_def disjoint_family_on_def image_subset_iff)
 
 lemma dynkin_subset:
   assumes "dynkin M"
@@ -41,7 +41,7 @@
   assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
   assumes "\<And> i :: nat. a i \<in> sets M"
   shows "UNION UNIV a \<in> sets M"
-using assms unfolding dynkin_def sorry
+using assms by (auto simp: dynkin_def disjoint_family_on_def image_subset_iff)
 
 definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"