changeset 11868 | 56db9f3a6b3e |
parent 11701 | 3d51fbf81c17 |
--- a/src/HOL/ex/IntRing.thy Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/ex/IntRing.thy Mon Oct 22 11:54:22 2001 +0200 @@ -10,7 +10,7 @@ IntRing = Ring + Lagrange + instance int :: add_semigroup (zadd_assoc) -instance int :: add_monoid (Zero_int_def,zadd_int0,zadd_int0_right) +instance int :: add_monoid (zadd_0,zadd_0_right) instance int :: add_group {|Auto_tac|} instance int :: add_agroup (zadd_commute) instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)