src/HOL/Library/Convex.thy
changeset 62376 85f38d5f8807
parent 61694 6571c78c9667
child 62418 f1b0908028cf
     1.1 --- a/src/HOL/Library/Convex.thy	Tue Feb 09 09:21:10 2016 +0100
     1.2 +++ b/src/HOL/Library/Convex.thy	Wed Feb 10 18:43:19 2016 +0100
     1.3 @@ -565,7 +565,7 @@
     1.4      then have "(\<Sum> j \<in> s. a j) = 0"
     1.5        using insert by auto
     1.6      then have "\<And>j. j \<in> s \<Longrightarrow> a j = 0"
     1.7 -      using setsum_nonneg_0[where 'b=real] insert by fastforce
     1.8 +      using insert by (fastforce simp: setsum_nonneg_eq_0_iff)
     1.9      then show ?thesis
    1.10        using insert by auto
    1.11    next