diff -r d007dee0c372 -r 7d0e10a961a6 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Apr 01 11:34:21 2009 -0700
+++ b/src/HOL/Int.thy	Wed Apr 01 22:29:27 2009 +0200
@@ -1382,8 +1382,6 @@
 
 subsection {* @{term setsum} and @{term setprod} *}
 
-text {*By Jeremy Avigad*}
-
 lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
   apply (cases "finite A")
   apply (erule finite_induct, auto)
@@ -1404,26 +1402,6 @@
   apply (erule finite_induct, auto)
   done
 
-lemma setprod_nonzero_nat:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::nat)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_pos_nat:
-  "finite S ==> (ALL x : S. f x > (0::nat)) ==> setprod f S > 0"
-using setprod_nonzero_nat by simp
-
-lemma setprod_zero_eq_nat:
-    "finite A ==> (setprod f A = (0::nat)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
-lemma setprod_nonzero_int:
-    "finite A ==> (\<forall>x \<in> A. f x \<noteq> (0::int)) ==> setprod f A \<noteq> 0"
-  by (rule setprod_nonzero, auto)
-
-lemma setprod_zero_eq_int:
-    "finite A ==> (setprod f A = (0::int)) = (\<exists>x \<in> A. f x = 0)"
-  by (rule setprod_zero_eq, auto)
-
 lemmas int_setsum = of_nat_setsum [where 'a=int]
 lemmas int_setprod = of_nat_setprod [where 'a=int]