# 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