diff -r 28b51effc5ed -r cdf7693bbe08 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Mar 14 14:37:47 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Mar 14 14:37:49 2011 +0100
@@ -1028,7 +1028,7 @@
   qed simp
 qed
 
-lemma setsum_of_pextreal:
+lemma setsum_real_of_extreal:
   assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
   shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
 proof -
@@ -1062,17 +1062,6 @@
     by induct (auto simp: extreal_right_distrib setsum_nonneg)
 qed simp
 
-lemma setsum_real_of_extreal:
-  assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
-  shows "real (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. real (f x))"
-proof cases
-  assume "finite A" from this assms show ?thesis
-  proof induct
-    case (insert a A) then show ?case
-      by (simp add: real_of_extreal_add setsum_Inf)
-  qed simp
-qed simp
-
 lemma sums_extreal_positive:
   fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" shows "f sums (SUP n. \<Sum>i<n. f i)"
 proof -