Replace algebra_eqI by algebra.equality;
Move sets_sigma_subset to Sigma_Algebra;

--- a/src/HOL/Probability/Borel_Space.thy	Wed Dec 01 19:42:09 2010 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Dec 01 20:09:41 2010 +0100
@@ -6,12 +6,6 @@
   imports Sigma_Algebra Positive_Infinite_Real Multivariate_Analysis
 begin
 
-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)
-
 lemma LIMSEQ_max:
   "u ----> (x::real) \<Longrightarrow> (\<lambda>i. max (u i) 0) ----> max x 0"
   by (fastsimp intro!: LIMSEQ_I dest!: LIMSEQ_D)
@@ -612,13 +606,10 @@
   then show ?thesis by (intro sets_sigma_subset) auto
 qed
 
-lemma algebra_eqI: assumes "sets A = sets (B::'a algebra)" "space A = space B"
-  shows "A = B" using assms by auto
-
 lemma borel_eq_atMost:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> a. {.. a::'a\<Colon>ordered_euclidean_space})\<rparr>)"
     (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets borel \<subseteq> sets ?SIGMA"
     using halfspace_le_span_atMost halfspace_span_halfspace_le open_span_halfspace
     by auto
@@ -629,7 +620,7 @@
 lemma borel_eq_atLeastAtMost:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space, b). {a .. b})\<rparr>)"
    (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets borel \<subseteq> sets ?SIGMA"
     using atMost_span_atLeastAtMost halfspace_le_span_atMost
       halfspace_span_halfspace_le open_span_halfspace
@@ -641,7 +632,7 @@
 lemma borel_eq_greaterThan:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {a <..})\<rparr>)"
    (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets borel \<subseteq> sets ?SIGMA"
     using halfspace_le_span_greaterThan
       halfspace_span_halfspace_le open_span_halfspace
@@ -653,7 +644,7 @@
 lemma borel_eq_lessThan:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a :: 'a\<Colon>ordered_euclidean_space). {..< a})\<rparr>)"
    (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets borel \<subseteq> sets ?SIGMA"
     using halfspace_le_span_lessThan
       halfspace_span_halfspace_ge open_span_halfspace
@@ -665,7 +656,7 @@
 lemma borel_eq_greaterThanLessThan:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, b). {a <..< (b :: 'a \<Colon> ordered_euclidean_space)})\<rparr>)"
     (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets ?SIGMA \<subseteq> sets borel"
     by (rule borel.sets_sigma_subset) auto
   show "sets borel \<subseteq> sets ?SIGMA"
@@ -686,7 +677,7 @@
 lemma borel_eq_halfspace_le:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i \<le> a})\<rparr>)"
    (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets borel \<subseteq> sets ?SIGMA"
     using open_span_halfspace halfspace_span_halfspace_le by auto
   show "sets ?SIGMA \<subseteq> sets borel"
@@ -696,7 +687,7 @@
 lemma borel_eq_halfspace_less:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. x$$i < a})\<rparr>)"
    (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets borel \<subseteq> sets ?SIGMA"
     using open_span_halfspace .
   show "sets ?SIGMA \<subseteq> sets borel"
@@ -706,7 +697,7 @@
 lemma borel_eq_halfspace_gt:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a < x$$i})\<rparr>)"
    (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets borel \<subseteq> sets ?SIGMA"
     using halfspace_le_span_halfspace_gt open_span_halfspace halfspace_span_halfspace_le by auto
   show "sets ?SIGMA \<subseteq> sets borel"
@@ -716,7 +707,7 @@
 lemma borel_eq_halfspace_ge:
   "borel = (sigma \<lparr>space=UNIV, sets=range (\<lambda> (a, i). {x::'a::ordered_euclidean_space. a \<le> x$$i})\<rparr>)"
    (is "_ = ?SIGMA")
-proof (rule algebra_eqI, rule antisym)
+proof (intro algebra.equality antisym)
   show "sets borel \<subseteq> sets ?SIGMA"
     using halfspace_span_halfspace_ge open_span_halfspace by auto
   show "sets ?SIGMA \<subseteq> sets borel"

--- 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)"