diff -r 28b51effc5ed -r cdf7693bbe08 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Mar 14 14:37:47 2011 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Mar 14 14:37:49 2011 +0100
@@ -1,7 +1,7 @@
-(*  Title:      HOL/Probability/Sigma_Algebra.thy
-    Author:     Stefan Richter
-    Author:     Markus Wenzel
-    Author:     Lawrence Paulson
+(*  Title:      Sigma_Algebra.thy
+    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
+    Plus material from the Hurd/Coble measure theory development,
+    translated by Lawrence Paulson.
 *)
 
 header {* Sigma Algebras *}
@@ -70,6 +70,16 @@
   "finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M"
   by (induct set: finite) (auto simp add: Un)
 
+lemma (in algebra) finite_UN[intro]:
+  assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
+  shows "(\<Union>i\<in>I. A i) \<in> sets M"
+  using assms by induct auto
+
+lemma (in algebra) finite_INT[intro]:
+  assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
+  shows "(\<Inter>i\<in>I. A i) \<in> sets M"
+  using assms by (induct rule: finite_ne_induct) auto
+
 lemma algebra_iff_Int:
      "algebra M \<longleftrightarrow>
        sets M \<subseteq> Pow (space M) & {} \<in> sets M &
@@ -149,11 +159,6 @@
   ultimately show ?thesis by simp
 qed
 
-lemma (in sigma_algebra) finite_UN:
-  assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
-  shows "(\<Union>i\<in>I. A i) \<in> sets M"
-  using assms by induct auto
-
 lemma (in sigma_algebra) countable_INT [intro]:
   fixes A :: "'i::countable \<Rightarrow> 'a set"
   assumes A: "A`X \<subseteq> sets M" "X \<noteq> {}"
@@ -167,11 +172,6 @@
   ultimately show ?thesis by metis
 qed
 
-lemma (in sigma_algebra) finite_INT:
-  assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M"
-  shows "(\<Inter>i\<in>I. A i) \<in> sets M"
-  using assms by (induct rule: finite_ne_induct) auto
-
 lemma algebra_Pow:
      "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
   by (auto simp add: algebra_def)