src/HOL/Rings.thy
changeset 58198 099ca49b5231
parent 58195 1fee63e0377d
child 58647 fce800afeec7
     1.1 --- a/src/HOL/Rings.thy	Sat Sep 06 20:12:36 2014 +0200
     1.2 +++ b/src/HOL/Rings.thy	Sun Sep 07 09:49:01 2014 +0200
     1.3 @@ -28,8 +28,6 @@
     1.4  class mult_zero = times + zero +
     1.5    assumes mult_zero_left [simp]: "0 * a = 0"
     1.6    assumes mult_zero_right [simp]: "a * 0 = 0"
     1.7 -
     1.8 -class semiring_0 = semiring + comm_monoid_add + mult_zero
     1.9  begin
    1.10  
    1.11  lemma mult_not_zero:
    1.12 @@ -38,6 +36,8 @@
    1.13  
    1.14  end
    1.15  
    1.16 +class semiring_0 = semiring + comm_monoid_add + mult_zero
    1.17 +
    1.18  class semiring_0_cancel = semiring + cancel_comm_monoid_add
    1.19  begin
    1.20