changeset 58198 | 099ca49b5231 |
parent 58195 | 1fee63e0377d |
child 58647 | fce800afeec7 |
--- a/src/HOL/Rings.thy Sat Sep 06 20:12:36 2014 +0200 +++ b/src/HOL/Rings.thy Sun Sep 07 09:49:01 2014 +0200 @@ -28,8 +28,6 @@ class mult_zero = times + zero + assumes mult_zero_left [simp]: "0 * a = 0" assumes mult_zero_right [simp]: "a * 0 = 0" - -class semiring_0 = semiring + comm_monoid_add + mult_zero begin lemma mult_not_zero: @@ -38,6 +36,8 @@ end +class semiring_0 = semiring + comm_monoid_add + mult_zero + class semiring_0_cancel = semiring + cancel_comm_monoid_add begin