diff -r b5e7594061ce -r 2e09299ce807 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jul 29 19:47:55 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Sat Jul 30 08:24:46 2011 +0200
@@ -397,10 +397,6 @@
 lemma affine_hull_eq[simp]: "(affine hull s = s) \<longleftrightarrow> affine s"
 by (metis affine_affine_hull hull_same mem_def)
 
-lemma setsum_restrict_set'': assumes "finite A"
-  shows "setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x  then f x else 0)"
-  unfolding mem_def[of _ P, symmetric] unfolding setsum_restrict_set'[OF assms] ..
-
 subsection {* Some explicit formulations (from Lars Schewe). *}
 
 lemma affine: fixes V::"'a::real_vector set"