--- 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"