src/HOL/Rings.thy
changeset 59910 815de5506080
parent 59865 8a20dd967385
child 60352 d46de31a50c4
     1.1 --- a/src/HOL/Rings.thy	Thu Apr 02 14:11:00 2015 +0200
     1.2 +++ b/src/HOL/Rings.thy	Thu Apr 02 11:22:22 2015 +0200
     1.3 @@ -502,7 +502,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class semidom = comm_semiring_1_cancel + semiring_no_zero_divisors
     1.8 +class semidom = comm_semiring_1_diff_distrib + semiring_no_zero_divisors
     1.9  
    1.10  class idom = comm_ring_1 + semiring_no_zero_divisors
    1.11  begin