generalized

--- 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