# HG changeset patch
# User haftmann
# Date 1427966542 -7200
# Node ID 815de5506080bf30a4c382e90acc85124519f442
# Parent  fbf4d5ad500d2ab735f441f9315ba8f130a923ab
semidom contains distributive minus, by convention

diff -r fbf4d5ad500d -r 815de5506080 src/HOL/Rings.thy
--- 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