src/HOL/Groups_Big.thy

--- a/src/HOL/Groups_Big.thy	Fri Apr 11 23:22:00 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Sat Apr 12 17:26:27 2014 +0200
@@ -1244,7 +1244,7 @@
 
 lemma setprod_pos [rule_format]: "(ALL x: A. (0::'a::linordered_semidom) < f x)
   --> 0 < setprod f A"
-by (cases "finite A", induct set: finite, simp_all add: mult_pos_pos)
+by (cases "finite A", induct set: finite, simp_all)
 
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
   (setprod f (A - {a}) :: 'a :: {field}) =