# HG changeset patch
# User haftmann
# Date 1410076141 -7200
# Node ID 099ca49b5231c1ccaf8360a09e64ae5625e7634d
# Parent  4fd7f47ead6ce1e8b8b9cc310ea696b60481be20
generalized

diff -r 4fd7f47ead6c -r 099ca49b5231 src/HOL/Rings.thy
--- 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