Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
semidom contains distributive minus, by convention
authorhaftmann
Thu, 02 Apr 2015 11:22:22 +0200
changeset 59910 815de5506080
parent 59909 fbf4d5ad500d
child 59911 0655a7217e14
semidom contains distributive minus, by convention
src/HOL/Rings.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Rings.thy	Thu Apr 02 14:11:00 2015 +0200
+++ b/src/HOL/Rings.thy	Thu Apr 02 11:22:22 2015 +0200
@@ -502,7 +502,7 @@
 
 end
 
-class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
+class semidom = comm_semiring_1_diff_distrib + semiring_no_zero_divisors
 
 class idom = comm_ring_1 + semiring_no_zero_divisors
 begin
isabelle