diff -r b21c820dfb63 -r b233f48a4d3d src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Mon Nov 09 15:50:31 2009 +0000
+++ b/src/HOL/Probability/Borel.thy	Mon Nov 09 16:06:08 2009 +0000
@@ -264,7 +264,7 @@
     by (simp add: borel_measurable_eq_borel_measurable compl_sets) 
 qed
 
-lemma (in measure_space) borel_measurable_plus_borel_measurable:
+lemma (in measure_space) borel_measurable_add_borel_measurable:
   assumes f: "f \<in> borel_measurable M"
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x + g x) \<in> borel_measurable M"
@@ -352,18 +352,18 @@
 proof -
   have 1: "(\<lambda>x. 0 + (f x + g x)\<twosuperior> * inverse 4) \<in> borel_measurable M"
     by (fast intro: affine_borel_measurable borel_measurable_square 
-                    borel_measurable_plus_borel_measurable f g) 
+                    borel_measurable_add_borel_measurable f g) 
   have "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) = 
         (\<lambda>x. 0 + ((f x + -g x) ^ 2 * inverse -4))"
     by (simp add: Ring_and_Field.minus_divide_right) 
   also have "... \<in> borel_measurable M" 
     by (fast intro: affine_borel_measurable borel_measurable_square 
-                    borel_measurable_plus_borel_measurable 
+                    borel_measurable_add_borel_measurable 
                     borel_measurable_uminus_borel_measurable f g)
   finally have 2: "(\<lambda>x. -((f x + -g x) ^ 2 * inverse 4)) \<in> borel_measurable M" .
   show ?thesis
     apply (simp add: times_eq_sum_squares real_diff_def) 
-    using 1 2 apply (simp add: borel_measurable_plus_borel_measurable) 
+    using 1 2 apply (simp add: borel_measurable_add_borel_measurable) 
     done
 qed
 
@@ -372,7 +372,7 @@
   assumes g: "g \<in> borel_measurable M"
   shows "(\<lambda>x. f x - g x) \<in> borel_measurable M"
 unfolding real_diff_def
-  by (fast intro: borel_measurable_plus_borel_measurable 
+  by (fast intro: borel_measurable_add_borel_measurable 
                   borel_measurable_uminus_borel_measurable f g)
 
 lemma (in measure_space) mono_convergent_borel_measurable:
@@ -409,7 +409,7 @@
     by (auto simp add: borel_measurable_le_iff) 
 qed
 
-lemma (in measure_space) borel_measurable_SIGMA_borel_measurable:
+lemma (in measure_space) borel_measurable_setsum_borel_measurable:
   assumes s: "finite s"
   shows "(!!i. i \<in> s ==> f i \<in> borel_measurable M) \<Longrightarrow> (\<lambda>x. setsum (\<lambda>i. f i x) s) \<in> borel_measurable M" using s
 proof (induct s)
@@ -419,7 +419,7 @@
 next
   case (insert x s)
   thus ?case
-    by (auto simp add: borel_measurable_plus_borel_measurable) 
+    by (auto simp add: borel_measurable_add_borel_measurable) 
 qed
 
 end