# HG changeset patch
# User hoelzl
# Date 1305821475 -7200
# Node ID 348fa5df7d3fb379b70f7effdfab88e08fcf48cb
# Parent  1e1b74448f6bfecd107db567a9a495cf43eab4e0
remove double sum_over_space_real_distribution

diff -r 1e1b74448f6b -r 348fa5df7d3f src/HOL/Probability/Probability_Measure.thy
--- a/src/HOL/Probability/Probability_Measure.thy	Thu May 19 18:09:20 2011 +0200
+++ b/src/HOL/Probability/Probability_Measure.thy	Thu May 19 18:11:15 2011 +0200
@@ -611,12 +611,6 @@
      (auto simp add: disjoint_family_on_def sets_eq_Pow
            intro!: arg_cong[where f=\<mu>'])
 
-lemma (in finite_prob_space) sum_over_space_real_distribution:
-  "(\<Sum>x\<in>X`space M. distribution X {x}) = 1"
-  unfolding distribution_def prob_space[symmetric] using finite_space
-  by (subst finite_measure_finite_Union[symmetric])
-     (auto simp add: disjoint_family_on_def sets_eq_Pow intro!: arg_cong[where f=prob])
-
 lemma (in finite_prob_space) finite_sum_over_space_eq_1:
   "(\<Sum>x\<in>space M. prob {x}) = 1"
   using prob_space finite_space