# HG changeset patch
# User wenzelm
# Date 1257792153 -3600
# Node ID fd28b7399f2ba3b172b3d30d24b205e1d1b07d88
# Parent  b233f48a4d3d8865a79fc813d0ceebc7f9a51427
eliminated hard tabulators;

diff -r b233f48a4d3d -r fd28b7399f2b src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Borel.thy	Mon Nov 09 19:42:33 2009 +0100
@@ -17,8 +17,8 @@
 
 definition mono_convergent where
   "mono_convergent u f s \<equiv>
-	(\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
-	(\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
+        (\<forall>x m n. m \<le> n \<and> x \<in> s \<longrightarrow> u m x \<le> u n x) \<and>
+        (\<forall>x \<in> s. (\<lambda>i. u i x) ----> f x)"
 
 lemma in_borel_measurable:
    "f \<in> borel_measurable M \<longleftrightarrow>
@@ -222,7 +222,7 @@
   shows "{w \<in> space M. f w < g w} \<in> sets M"
 proof -
   have "{w \<in> space M. f w < g w} =
-	(\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
+        (\<Union>r\<in>\<rat>. {w \<in> space M. f w < r} \<inter> {w \<in> space M. r < g w })"
     by (auto simp add: Rats_dense_in_real)
   thus ?thesis using f g 
     by (simp add: borel_measurable_less_iff [of f]  
@@ -247,7 +247,7 @@
   shows "{w \<in> space M. f w = g w} \<in> sets M"
 proof -
   have "{w \<in> space M. f w = g w} =
-	{w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
+        {w \<in> space M. f w \<le> g w} \<inter> {w \<in> space M. g w \<le> f w}"
     by auto
   thus ?thesis using f g 
     by (simp add: borel_measurable_leq_borel_measurable Int) 
diff -r b233f48a4d3d -r fd28b7399f2b src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Caratheodory.thy	Mon Nov 09 19:42:33 2009 +0100
@@ -2,7 +2,6 @@
 
 theory Caratheodory
   imports Sigma_Algebra SupInf SeriesPlus
-
 begin
 
 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -136,7 +135,7 @@
     proof 
       fix n
       show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
-	by (induct n)  (auto simp add: binaryset_def f) 
+        by (induct n)  (auto simp add: binaryset_def f) 
     qed
   moreover
   have "... ----> f A + f B" by (rule LIMSEQ_const) 
@@ -198,30 +197,30 @@
   proof -
     from xl yl show ?thesis
       proof (auto simp add: positive_def lambda_system_eq Int)
-	fix u
-	assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
+        fix u
+        assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
            and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
            and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
-	have "u - x \<inter> y \<in> sets M"
-	  by (metis Diff Diff_Int Un u x y)
-	moreover
-	have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
-	moreover
-	have "u - x \<inter> y - y = u - y" by blast
-	ultimately
-	have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
-	  by force
-	have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) 
+        have "u - x \<inter> y \<in> sets M"
+          by (metis Diff Diff_Int Un u x y)
+        moreover
+        have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
+        moreover
+        have "u - x \<inter> y - y = u - y" by blast
+        ultimately
+        have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
+          by force
+        have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) 
               = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
-	  by (simp add: ey) 
-	also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
-	  by (simp add: Int_ac) 
-	also have "... = f (u \<inter> y) + f (u - y)"
-	  using fx [THEN bspec, of "u \<inter> y"] Int y u
-	  by force
-	also have "... = f u"
-	  by (metis fy u) 
-	finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
+          by (simp add: ey) 
+        also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
+          by (simp add: Int_ac) 
+        also have "... = f (u \<inter> y) + f (u - y)"
+          using fx [THEN bspec, of "u \<inter> y"] Int y u
+          by force
+        also have "... = f u"
+          by (metis fy u) 
+        finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
       qed
   qed
 
@@ -478,11 +477,11 @@
   have U_eq: "f (\<Union>i. A i) = suminf (f o A)" 
     proof (rule antisym)
       show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
-	by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) 
+        by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) 
       show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
-	by (rule suminf_le [OF sumfA]) 
+        by (rule suminf_le [OF sumfA]) 
            (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
-	          lambda_system_positive lambda_system_additive 
+                  lambda_system_positive lambda_system_additive 
                   subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) 
     qed
   {
@@ -491,58 +490,58 @@
     have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
     proof -
       have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A'' 
-	apply -
-	apply (rule summable_comparison_test [OF _ sumfA]) 
-	apply (rule_tac x="0" in exI) 
-	apply (simp add: positive_def) 
-	apply (auto simp add: )
-	apply (subst abs_of_nonneg)
-	apply (metis A'' Int UNIV_I a image_subset_iff)
-	apply (blast intro:  increasingD [OF inc] a)   
-	done
+        apply -
+        apply (rule summable_comparison_test [OF _ sumfA]) 
+        apply (rule_tac x="0" in exI) 
+        apply (simp add: positive_def) 
+        apply (auto simp add: )
+        apply (subst abs_of_nonneg)
+        apply (metis A'' Int UNIV_I a image_subset_iff)
+        apply (blast intro:  increasingD [OF inc] a)   
+        done
       show ?thesis
       proof (rule antisym)
-	have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
-	  by blast
-	moreover 
-	have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
-	  by (auto simp add: disjoint_family_def) 
-	moreover 
-	have "a \<inter> (\<Union>i. A i) \<in> sets M"
-	  by (metis Int U_in a)
-	ultimately 
-	have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
-	  using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
-	  by (simp add: o_def) 
-	moreover 
-	have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
-	  proof (rule suminf_le [OF summ])
-	    fix n
-	    have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
-	      by (metis A'' UNION_in_sets) 
-	    have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
-	      by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) 
-	    have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
-	      using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
-	      by (simp add: A) 
-	    hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
-	      by (simp add: lambda_system_eq UNION_in Diff_Compl a)
-	    have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
-	      by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image 
+        have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
+          by blast
+        moreover 
+        have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
+          by (auto simp add: disjoint_family_def) 
+        moreover 
+        have "a \<inter> (\<Union>i. A i) \<in> sets M"
+          by (metis Int U_in a)
+        ultimately 
+        have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
+          using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
+          by (simp add: o_def) 
+        moreover 
+        have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
+          proof (rule suminf_le [OF summ])
+            fix n
+            have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
+              by (metis A'' UNION_in_sets) 
+            have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
+              by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) 
+            have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
+              using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
+              by (simp add: A) 
+            hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
+              by (simp add: lambda_system_eq UNION_in Diff_Compl a)
+            have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
+              by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image 
                                UNION_in U_in a) 
-	    thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
-	      using eq_fa
-	      by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos 
+            thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
+              using eq_fa
+              by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos 
                             a A disj)
-	  qed
-	ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" 
-	  by arith
+          qed
+        ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" 
+          by arith
       next
-	have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" 
-	  by (blast intro:  increasingD [OF inc] a U_in)
-	also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
-	  by (blast intro: subadditiveD [OF sa] Int Diff U_in) 
-	finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
+        have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" 
+          by (blast intro:  increasingD [OF inc] a U_in)
+        also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
+          by (blast intro: subadditiveD [OF sa] Int Diff U_in) 
+        finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
         qed
      qed
   }
@@ -654,20 +653,20 @@
   have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
     proof (rule countably_additiveD [OF ca]) 
       show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
-	by blast
+        by blast
       show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
-	by (auto simp add: disjoint_family_def)
+        by (auto simp add: disjoint_family_def)
       show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
-	by (metis UN_extend_simps(4) s seq)
+        by (metis UN_extend_simps(4) s seq)
     qed
   hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
     by (metis Int_commute UN_simps(4) seq sums_iff) 
   also have "... \<le> suminf (f \<circ> A)" 
     proof (rule summable_le [OF _ _ sm]) 
       show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
-	by (force intro: increasingD [OF inc]) 
+        by (force intro: increasingD [OF inc]) 
       show "summable (\<lambda>i. f (A i \<inter> s))" using sums
-	by (simp add: sums_iff) 
+        by (simp add: sums_iff) 
     qed
   also have "... = z" by (rule si) 
   finally show "f s \<le> z" .
@@ -722,9 +721,9 @@
     proof (auto)
       fix n
       have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
-	by (auto simp add: positive_def image_subset_iff)
+        by (auto simp add: positive_def image_subset_iff)
       also have "... \<le> f (A n)" 
-	by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
+        by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
       finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
     qed
   from Series.summable_le2 [OF this sm]
@@ -787,32 +786,32 @@
         and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
       by auto blast
     have llpos: "!!n. 0 \<le> ll n"
-	by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero 
+        by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero 
               range_subsetD BB) 
     have sll: "summable ll &
                suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
       proof -
-	have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
-	  by (rule sums_mult [OF power_half_series]) 
-	hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
-	  and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
-	  by (auto simp add: sums_iff) 
-	have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
+        have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
+          by (rule sums_mult [OF power_half_series]) 
+        hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
+          and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
+          by (auto simp add: sums_iff) 
+        have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
                  suminf (\<lambda>n. e * (1/2)^(Suc n)) =
                  suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
-	  by (rule suminf_add [OF sum1 sum0]) 
-	have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
-	  by (metis ll llpos abs_of_nonneg)
-	have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
-	  by (rule summable_add [OF sum1 sum0]) 
-	have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
-	  using Series.summable_le2 [OF 1 2] by auto
-	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + 
+          by (rule suminf_add [OF sum1 sum0]) 
+        have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
+          by (metis ll llpos abs_of_nonneg)
+        have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
+          by (rule summable_add [OF sum1 sum0]) 
+        have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
+          using Series.summable_le2 [OF 1 2] by auto
+        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + 
                          (\<Sum>n. e * (1 / 2) ^ Suc n)"
-	  by (metis 0) 
-	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
-	  by (simp add: eqe) 
-	finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
+          by (metis 0) 
+        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
+          by (simp add: eqe) 
+        finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
       qed
     def C \<equiv> "(split BB) o nat_to_nat2"
     have C: "!!n. C n \<in> sets M"
@@ -822,24 +821,24 @@
       done
     have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
       proof (auto simp add: C_def)
-	fix x i
-	assume x: "x \<in> A i"
-	with sbBB [of i] obtain j where "x \<in> BB i j"
-	  by blast	  
-	thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
-	  by (metis nat_to_nat2_surj internal_split_def prod.cases 
+        fix x i
+        assume x: "x \<in> A i"
+        with sbBB [of i] obtain j where "x \<in> BB i j"
+          by blast        
+        thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
+          by (metis nat_to_nat2_surj internal_split_def prod.cases 
                 prod_case_split surj_f_inv_f)
       qed 
     have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
       by (rule ext)  (auto simp add: C_def) 
     also have "... sums suminf ll" 
       proof (rule suminf_2dimen)
-	show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB 
-	  by (force simp add: positive_def)
-	show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
-	  by (force simp add: o_def)
-	show "summable ll" using sll
-	  by auto
+        show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB 
+          by (force simp add: positive_def)
+        show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
+          by (force simp add: o_def)
+        show "summable ll" using sll
+          by auto
       qed
     finally have Csums: "(f \<circ> C) sums suminf ll" .
     have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
@@ -882,24 +881,24 @@
       from inf_measure_close [OF posf e s]
       obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
                    and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
-	           and l: "l \<le> Inf (measure_set M f s) + e"
-	by auto
+                   and l: "l \<le> Inf (measure_set M f s) + e"
+        by auto
       have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
                       (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
-	by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
+        by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
       have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
-	by (subst additiveD [OF add, symmetric])
- 	   (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
+        by (subst additiveD [OF add, symmetric])
+           (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
       have fsumb: "summable (f \<circ> A)"
-	by (metis fsums sums_iff) 
+        by (metis fsums sums_iff) 
       { fix u
-	assume u: "u \<in> sets M"
-	have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
-	  by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc] 
+        assume u: "u \<in> sets M"
+        have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
+          by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc] 
                         u Int  range_subsetD [OF A]) 
-	have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" 
+        have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" 
           by (rule summable_comparison_test [OF _ fsumb]) simp
-	have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
+        have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
           proof (rule Inf_lower) 
             show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
               apply (simp add: measure_set_def) 
@@ -920,14 +919,14 @@
         and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
         and inf2: "Inf (measure_set M f (s \<inter> (space M - x))) 
                    \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
-	by (metis Diff lesum top x)+
+        by (metis Diff lesum top x)+
       hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
            \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
-	by (simp add: x)
+        by (simp add: x)
       also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2] 
-	by (simp add: x) (simp add: o_def) 
+        by (simp add: x) (simp add: o_def) 
       also have "... \<le> Inf (measure_set M f s) + e"
-	by (metis fsums l sums_unique) 
+        by (metis fsums l sums_unique) 
       finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
         \<le> Inf (measure_set M f s) + e" .
     qed
@@ -940,7 +939,7 @@
     also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" 
       apply (rule subadditiveD) 
       apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow 
-	       inf_measure_positive inf_measure_countably_subadditive posf inc)
+               inf_measure_positive inf_measure_countably_subadditive posf inc)
       apply (auto simp add: subsetD [OF s])  
       done
     finally show ?thesis .
diff -r b233f48a4d3d -r fd28b7399f2b src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Measure.thy	Mon Nov 09 19:42:33 2009 +0100
@@ -46,8 +46,8 @@
 definition
   measurable  where
   "measurable a b = {f . sigma_algebra a & sigma_algebra b &
-			 f \<in> (space a -> space b) &
-			 (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
+                         f \<in> (space a -> space b) &
+                         (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
 
 definition
   measure_preserving  where
@@ -258,23 +258,23 @@
       fix x
       assume x: "x \<in> smallest_ccdi_sets M"
       thus "x \<in> C"
-	proof (induct rule: smallest_ccdi_sets.induct)
-	  case (Basic x)
-	  thus ?case
-	    by (metis Basic subsetD sbC)
-	next
-	  case (Compl x)
-	  thus ?case
-	    by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
- 	next
-	  case (Inc A)
-	  thus ?case
-	       by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) 
-	next
-	  case (Disj A)
-	  thus ?case
-	       by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) 
-	qed
+        proof (induct rule: smallest_ccdi_sets.induct)
+          case (Basic x)
+          thus ?case
+            by (metis Basic subsetD sbC)
+        next
+          case (Compl x)
+          thus ?case
+            by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
+        next
+          case (Inc A)
+          thus ?case
+               by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) 
+        next
+          case (Disj A)
+          thus ?case
+               by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) 
+        qed
     qed
   finally show ?thesis .
 qed
@@ -292,12 +292,12 @@
   have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)" 
     proof (rule sigma_property_disjoint_lemma) 
       show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
-	by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
+        by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
     next
       show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
-	by (simp add: closed_cdi_def compl inc disj)
+        by (simp add: closed_cdi_def compl inc disj)
            (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
-	     IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
+             IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
     qed
   thus ?thesis
     by blast
@@ -349,7 +349,7 @@
       case 0 show ?case by simp
     next
       case (Suc m) thus ?case
-	by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
+        by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
     qed
   }
   hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
@@ -371,17 +371,17 @@
     have "(measure M \<circ> A) n =
           setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
       proof (induct n)
-	case 0 thus ?case by (auto simp add: A0 empty_measure)
+        case 0 thus ?case by (auto simp add: A0 empty_measure)
       next
-	case (Suc m) 
-	have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
-	  by (metis ASuc Un_Diff_cancel Un_absorb1)
-	hence "measure M (A (Suc m)) =
+        case (Suc m) 
+        have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
+          by (metis ASuc Un_Diff_cancel Un_absorb1)
+        hence "measure M (A (Suc m)) =
                measure M (A m) + measure M (A (Suc m) - A m)" 
-	  by (subst measure_additive) 
+          by (subst measure_additive) 
              (auto simp add: measure_additive range_subsetD [OF A]) 
-	with Suc show ?case
-	  by simp
+        with Suc show ?case
+          by simp
       qed
   }
   hence Meq: "measure M o A = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
@@ -390,13 +390,13 @@
     proof (rule UN_finite2_eq [where k=1], simp) 
       fix i
       show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
-	proof (induct i)
-	  case 0 thus ?case by (simp add: A0)
-	next
-	  case (Suc i) 
-	  thus ?case
-	    by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
-	qed
+        proof (induct i)
+          case 0 thus ?case by (simp add: A0)
+        next
+          case (Suc i) 
+          thus ?case
+            by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
+        qed
     qed
   have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
     by (metis A Diff range_subsetD)
@@ -461,23 +461,23 @@
     assume A: "range A \<subseteq> (vimage f) ` (sets b)"
     have  "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
       proof -
-	def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
-	{ 
-	  fix i
-	  have "A i \<in> (vimage f) ` (sets b)" using A
-	    by blast
-	  hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
-	    by blast
-	  hence "B i \<in> sets b \<and> f -` B i = A i" 
-	    by (simp add: B_def) (erule someI_ex)
-	} note B = this
-	show ?thesis
-	  proof
-	    show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
-	      by (simp add: vimage_UN B) 
-	   show "(\<Union>i. B i) \<in> sets b" using B
-	     by (auto intro: sigma_algebra.countable_UN [OF b]) 
-	  qed
+        def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
+        { 
+          fix i
+          have "A i \<in> (vimage f) ` (sets b)" using A
+            by blast
+          hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
+            by blast
+          hence "B i \<in> sets b \<and> f -` B i = A i" 
+            by (simp add: B_def) (erule someI_ex)
+        } note B = this
+        show ?thesis
+          proof
+            show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
+              by (simp add: vimage_UN B) 
+           show "(\<Union>i. B i) \<in> sets b" using B
+             by (auto intro: sigma_algebra.countable_UN [OF b]) 
+          qed
       qed
   }
   thus "\<forall>A::nat \<Rightarrow> 'a set.
@@ -496,26 +496,26 @@
       fix x
       assume "x \<in> sigma_sets X B"
       thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
-	proof induct
-	  case (Basic a)
-	  thus ?case
-	    by (auto simp add: ba) (metis B subsetD PowD) 
+        proof induct
+          case (Basic a)
+          thus ?case
+            by (auto simp add: ba) (metis B subsetD PowD) 
         next
-	  case Empty
-	  thus ?case
-	    by auto
+          case Empty
+          thus ?case
+            by auto
         next
-	  case (Compl a)
-	  have [simp]: "f -` X \<inter> space M = space M"
-	    by (auto simp add: funcset_mem [OF f]) 
-	  thus ?case
-	    by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
-	next
-	  case (Union a)
-	  thus ?case
-	    by (simp add: vimage_UN, simp only: UN_extend_simps(4))
-	       (blast intro: countable_UN)
-	qed
+          case (Compl a)
+          have [simp]: "f -` X \<inter> space M = space M"
+            by (auto simp add: funcset_mem [OF f]) 
+          thus ?case
+            by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
+        next
+          case (Union a)
+          thus ?case
+            by (simp add: vimage_UN, simp only: UN_extend_simps(4))
+               (blast intro: countable_UN)
+        qed
     qed
   thus ?thesis
     by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) 
@@ -553,122 +553,122 @@
   show ?thesis using fmp
     proof (clarsimp simp add: measure_preserving_def m1 m2) 
       assume fm: "f \<in> measurable m1 (m a)" 
-	 and mam: "measure_space (m a)"
-	 and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
+         and mam: "measure_space (m a)"
+         and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
       have "f \<in> measurable m1 (sigma (space (m a)) (sets (m a)))"
-	by (rule subsetD [OF measurable_subset fm]) 
+        by (rule subsetD [OF measurable_subset fm]) 
       also have "... = measurable m1 m2"
-	by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def) 
+        by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def) 
       finally have f12: "f \<in> measurable m1 m2" .
       hence ffn: "f \<in> space m1 \<rightarrow> space m2"
-	by (simp add: measurable_def) 
+        by (simp add: measurable_def) 
       have "space m1 \<subseteq> f -` (space m2)"
-	by auto (metis PiE ffn)
+        by auto (metis PiE ffn)
       hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
-	by blast
+        by blast
       {
-	fix y
-	assume y: "y \<in> sets m2" 
-	have ama: "algebra (m a)"  using mam
-	  by (simp add: measure_space_def sigma_algebra_iff) 
-	have spa: "space m2 \<in> a" using algebra.top [OF ama]
-	  by (simp add: m_def) 
-	have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
-	  by (simp add: m_def) 
-	also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
-	  proof (rule algebra.sigma_property_disjoint, auto simp add: ama) 
-	    fix x
-	    assume x: "x \<in> a"
-	    thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
-	      by (simp add: meq)
-	  next
-	    fix s
-	    assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
-	       and s: "s \<in> sigma_sets (space m2) a"
-	    hence s2: "s \<in> sets m2"
-	      by (simp add: setsm2) 
-	    thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
+        fix y
+        assume y: "y \<in> sets m2" 
+        have ama: "algebra (m a)"  using mam
+          by (simp add: measure_space_def sigma_algebra_iff) 
+        have spa: "space m2 \<in> a" using algebra.top [OF ama]
+          by (simp add: m_def) 
+        have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
+          by (simp add: m_def) 
+        also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
+          proof (rule algebra.sigma_property_disjoint, auto simp add: ama) 
+            fix x
+            assume x: "x \<in> a"
+            thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
+              by (simp add: meq)
+          next
+            fix s
+            assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
+               and s: "s \<in> sigma_sets (space m2) a"
+            hence s2: "s \<in> sets m2"
+              by (simp add: setsm2) 
+            thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
                   measure m2 (space m2 - s)" using f12
-	      by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
-		    measure_space.measure_compl measurable_def)  
-	         (metis fveq meq spa) 
-	  next
-	    fix A
-	      assume A0: "A 0 = {}"
-	 	 and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
-		 and rA1: "range A \<subseteq> 
-		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
-		 and "range A \<subseteq> sigma_sets (space m2) a"
-	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
-	      have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
-		using rA1 by blast
-	      have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))" 
-		by (simp add: o_def eq1) 
-	      also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
-		proof (rule measure_space.measure_countable_increasing [OF m1])
-		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
-		    using f12 rA2 by (auto simp add: measurable_def)
-		  show "f -` A 0 \<inter> space m1 = {}" using A0
-		    by blast
-		  show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
-		    using ASuc by auto
-		qed
-	      also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
-		by (simp add: vimage_UN)
-	      finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
-	      moreover
-	      have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
-		by (rule measure_space.measure_countable_increasing 
-		          [OF m2 rA2, OF A0 ASuc])
-	      ultimately 
-	      show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+              by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
+                    measure_space.measure_compl measurable_def)  
+                 (metis fveq meq spa) 
+          next
+            fix A
+              assume A0: "A 0 = {}"
+                 and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
+                 and rA1: "range A \<subseteq> 
+                           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+                 and "range A \<subseteq> sigma_sets (space m2) a"
+              hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+              have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+                using rA1 by blast
+              have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))" 
+                by (simp add: o_def eq1) 
+              also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+                proof (rule measure_space.measure_countable_increasing [OF m1])
+                  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+                    using f12 rA2 by (auto simp add: measurable_def)
+                  show "f -` A 0 \<inter> space m1 = {}" using A0
+                    by blast
+                  show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
+                    using ASuc by auto
+                qed
+              also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
+                by (simp add: vimage_UN)
+              finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
+              moreover
+              have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
+                by (rule measure_space.measure_countable_increasing 
+                          [OF m2 rA2, OF A0 ASuc])
+              ultimately 
+              show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
                     measure m2 (\<Union>i. A i)"
-		by (rule LIMSEQ_unique) 
-	  next
-	    fix A :: "nat => 'a2 set"
-	      assume dA: "disjoint_family A"
-		 and rA1: "range A \<subseteq> 
-		           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
-		 and "range A \<subseteq> sigma_sets (space m2) a"
-	      hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
-	      hence Um2: "(\<Union>i. A i) \<in> sets m2"
-		by (metis range_subsetD setsm2 sigma_sets.Union)
-	      have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
-		using rA1 by blast
-	      hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
-		by (simp add: o_def) 
-	      also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" 
-		proof (rule measure_space.measure_countably_additive [OF m1] )
-		  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
-		    using f12 rA2 by (auto simp add: measurable_def)
-		  show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
-		    by (auto simp add: disjoint_family_def) 
-		  show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
-		    proof (rule sigma_algebra.countable_UN [OF sa1])
-		      show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
-			by (auto simp add: measurable_def) 
-		    qed
- 		qed
-	      finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
-	      with measure_space.measure_countably_additive [OF m2 rA2 dA Um2] 
-	      have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
-		by (metis sums_unique) 
+                by (rule LIMSEQ_unique) 
+          next
+            fix A :: "nat => 'a2 set"
+              assume dA: "disjoint_family A"
+                 and rA1: "range A \<subseteq> 
+                           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
+                 and "range A \<subseteq> sigma_sets (space m2) a"
+              hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
+              hence Um2: "(\<Union>i. A i) \<in> sets m2"
+                by (metis range_subsetD setsm2 sigma_sets.Union)
+              have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
+                using rA1 by blast
+              hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
+                by (simp add: o_def) 
+              also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" 
+                proof (rule measure_space.measure_countably_additive [OF m1] )
+                  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
+                    using f12 rA2 by (auto simp add: measurable_def)
+                  show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
+                    by (auto simp add: disjoint_family_def) 
+                  show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
+                    proof (rule sigma_algebra.countable_UN [OF sa1])
+                      show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
+                        by (auto simp add: measurable_def) 
+                    qed
+                qed
+              finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
+              with measure_space.measure_countably_additive [OF m2 rA2 dA Um2] 
+              have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
+                by (metis sums_unique) 
 
-	      moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
-		by (simp add: vimage_UN)
-	      ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
+              moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
+                by (simp add: vimage_UN)
+              ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
                     measure m2 (\<Union>i. A i)" 
-		by metis
-	  qed
-	finally have "sigma_sets (space m2) a 
+                by metis
+          qed
+        finally have "sigma_sets (space m2) a 
               \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
-	hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
-	  by (force simp add: setsm2) 
+        hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
+          by (force simp add: setsm2) 
       }
       thus "f \<in> measurable m1 m2 \<and>
        (\<forall>y\<in>sets m2.
            measure m1 (f -` y \<inter> space m1) = measure m2 y)"
-	by (blast intro: f12) 
+        by (blast intro: f12) 
     qed
 qed
 
diff -r b233f48a4d3d -r fd28b7399f2b src/HOL/Probability/Probability.thy
--- a/src/HOL/Probability/Probability.thy	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Probability.thy	Mon Nov 09 19:42:33 2009 +0100
@@ -1,5 +1,5 @@
-theory Probability imports
-	Measure
+theory Probability
+imports Measure
 begin
 
 end
diff -r b233f48a4d3d -r fd28b7399f2b src/HOL/Probability/ROOT.ML
--- a/src/HOL/Probability/ROOT.ML	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/ROOT.ML	Mon Nov 09 19:42:33 2009 +0100
@@ -1,6 +1,1 @@
-(*
-  no_document use_thy "ThisTheory";
-  use_thy "ThatTheory";
-*)
-
 use_thy "Probability";
diff -r b233f48a4d3d -r fd28b7399f2b src/HOL/Probability/SeriesPlus.thy
--- a/src/HOL/Probability/SeriesPlus.thy	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/SeriesPlus.thy	Mon Nov 09 19:42:33 2009 +0100
@@ -1,6 +1,5 @@
 theory SeriesPlus
   imports Complex_Main Nat_Int_Bij 
-
 begin
 
 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
@@ -28,9 +27,9 @@
     proof -
       fix m
       have "0 \<le> suminf (\<lambda>n. f (m,n))"
-	by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
+        by (rule suminf_0_le, simp add: f_nneg, metis fsums sums_iff)
       thus "0 \<le> g m" using fsums [of m] 
-	by (auto simp add: sums_iff) 
+        by (auto simp add: sums_iff) 
     qed
   show "(\<lambda>n. \<Sum>x = 0..<n. f (nat_to_nat2 x)) ----> suminf g"
   proof (rule increasing_LIMSEQ, simp add: f_nneg)
@@ -48,14 +47,14 @@
       by (rule setsum_mono2) (auto simp add: ij) 
     also have "... = setsum (\<lambda>m. setsum (\<lambda>n. f (m,n)) {0..j}) {0..<Suc i}"
       by (metis atLeast0AtMost atLeast0LessThan lessThan_Suc_atMost
-	        setsum_cartesian_product split_eta) 
+                setsum_cartesian_product split_eta) 
     also have "... \<le> setsum g {0..<Suc i}" 
       proof (rule setsum_mono, simp add: less_Suc_eq_le) 
-	fix m
-	assume m: "m \<le> i"
-	thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
-	  by (auto simp add: sums_iff) 
-	   (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg) 
+        fix m
+        assume m: "m \<le> i"
+        thus " (\<Sum>n = 0..j. f (m, n)) \<le> g m" using fsums [of m]
+          by (auto simp add: sums_iff) 
+           (metis atLeastLessThanSuc_atLeastAtMost f_nneg series_pos_le f_nneg) 
       qed
     finally have  "(\<Sum>x = 0..<n. f (nat_to_nat2 x)) \<le> setsum g {0..<Suc i}" .
     also have "... \<le> suminf g" 
@@ -73,13 +72,13 @@
     { fix m
       assume m: "m<N"
       hence enneg: "0 < e / (2 * real N)" using e
-	by (simp add: zero_less_divide_iff) 
+        by (simp add: zero_less_divide_iff) 
       hence  "\<exists>j. \<bar>(\<Sum>n = 0..<j. f (m, n)) - g m\<bar> < e/(2 * real N)"
-	using fsums [of m] m
+        using fsums [of m] m
         by (force simp add: sums_def LIMSEQ_def dist_real_def)
       hence "\<exists>j. g m < setsum (\<lambda>n. f (m,n)) {0..<j} + e/(2 * real N)" 
-	using fsums [of m]
-	by (auto simp add: sums_iff) 
+        using fsums [of m]
+        by (auto simp add: sums_iff) 
            (metis abs_diff_less_iff add_less_cancel_right eq_diff_eq') 
     }
     hence "\<exists>jj. \<forall>m. m<N \<longrightarrow> g m < (\<Sum>n = 0..<jj m. f (m, n)) + e/(2 * real N)"
@@ -103,13 +102,13 @@
     def NIJ \<equiv> "Max (nat_to_nat2 -` IJ)"
     have IJsb: "IJ \<subseteq> nat_to_nat2 ` {0..NIJ}"
       proof (auto simp add: NIJ_def)
-	fix i j
-	assume ij:"(i,j) \<in> IJ"
-	hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
-	  by (metis nat_to_nat2_surj surj_f_inv_f) 
-	thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
-	  by (rule image_eqI) 
-	     (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
+        fix i j
+        assume ij:"(i,j) \<in> IJ"
+        hence "(i,j) = nat_to_nat2 (inv nat_to_nat2 (i,j))"
+          by (metis nat_to_nat2_surj surj_f_inv_f) 
+        thus "(i,j) \<in> nat_to_nat2 ` {0..Max (nat_to_nat2 -` IJ)}"
+          by (rule image_eqI) 
+             (simp add: ij finite_vimageI [OF finite_IJ nat_to_nat2_inj]
                     nat_to_nat2_surj surj_f_inv_f) 
       qed
     have "setsum f IJ \<le> setsum f (nat_to_nat2 `{0..NIJ})"
diff -r b233f48a4d3d -r fd28b7399f2b src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 09 19:42:33 2009 +0100
@@ -235,4 +235,3 @@
   by (simp add: sigma_def sigma_sets_subset)
 
 end
-
diff -r b233f48a4d3d -r fd28b7399f2b src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Nov 09 16:06:08 2009 +0000
+++ b/src/HOL/Series.thy	Mon Nov 09 19:42:33 2009 +0100
@@ -293,11 +293,11 @@
   have "convergent (\<lambda>n. setsum f {0..<n})" 
     proof (rule Bseq_mono_convergent)
       show "Bseq (\<lambda>n. setsum f {0..<n})"
-	by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
+        by (rule f_inc_g_dec_Beq_f [of "(\<lambda>n. setsum f {0..<n})" "\<lambda>n. x"])
            (auto simp add: le pos)  
     next 
       show "\<forall>m n. m \<le> n \<longrightarrow> setsum f {0..<m} \<le> setsum f {0..<n}"
-	by (auto intro: setsum_mono2 pos) 
+        by (auto intro: setsum_mono2 pos) 
     qed
   then obtain L where "(%n. setsum f {0..<n}) ----> L"
     by (blast dest: convergentD)