diff -r 34b3366b83ac -r b6456ccd9e3e src/HOL/ex/IntRing.thy --- a/src/HOL/ex/IntRing.thy Thu Oct 01 18:29:53 1998 +0200 +++ b/src/HOL/ex/IntRing.thy Thu Oct 01 18:30:05 1998 +0200 @@ -10,7 +10,7 @@ IntRing = IntRingDefs + Lagrange + instance int :: add_semigroup (zadd_assoc) -instance int :: add_monoid (zero_int_def,zadd_0,zadd_0_right) +instance int :: add_monoid (zero_int_def,zadd_nat0,zadd_nat0_right) instance int :: add_group (left_inv_int,minus_inv_int) instance int :: add_agroup (zadd_commute) instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)