src/HOL/Library/Euclidean_Space.thy
changeset 31034 736f521ad036
parent 31021 53642251a04f
child 31118 541d43bee678
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon May 04 14:49:48 2009 +0200
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon May 04 14:49:49 2009 +0200
     1.3 @@ -593,7 +593,7 @@
     1.4    from insert.prems have Fx: "f x \<ge> 0" and Fp: "\<forall> a \<in> F. f a \<ge> 0" by simp_all
     1.5    from insert.hyps Fp setsum_nonneg[OF Fp]
     1.6    have h: "setsum f F = 0 \<longleftrightarrow> (\<forall>a \<in>F. f a = 0)" by metis
     1.7 -  from sum_nonneg_eq_zero_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)
     1.8 +  from add_nonneg_eq_0_iff[OF Fx  setsum_nonneg[OF Fp]] insert.hyps(1,2)
     1.9    show ?case by (simp add: h)
    1.10  qed
    1.11