Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Groups_Big.thy
changeset 59833 ab828c2c5d67
parent 59615 fdfdf89a83a6
child 59867 58043346ca64 
--- a/src/HOL/Groups_Big.thy	Sat Mar 28 20:43:19 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Sat Mar 28 21:32:48 2015 +0100
@@ -1150,7 +1150,7 @@
 
 lemma setprod_zero_iff [simp]:
   assumes "finite A"
-  shows "setprod f A = (0::'a::{comm_semiring_1,no_zero_divisors}) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
+  shows "setprod f A = (0::'a::semidom) \<longleftrightarrow> (\<exists>a\<in>A. f a = 0)"
   using assms by (induct A) (auto simp: no_zero_divisors)
 
 lemma (in field) setprod_diff1:
isabelle