diff -r 548901d05a0e -r a1c426541757 src/HOL/ex/IntRing.thy
--- a/src/HOL/ex/IntRing.thy	Tue May 23 18:06:22 2000 +0200
+++ b/src/HOL/ex/IntRing.thy	Tue May 23 18:08:52 2000 +0200
@@ -7,11 +7,11 @@
 With an application of Lagrange's lemma.
 *)
 
-IntRing = IntRingDefs + Lagrange +
+IntRing = Ring + Lagrange +
 
 instance int :: add_semigroup (zadd_assoc)
-instance int :: add_monoid (zero_int_def,zadd_int0,zadd_int0_right)
-instance int :: add_group (left_inv_int,minus_inv_int)
+instance int :: add_monoid (IntDef.Zero_def,zadd_int0,zadd_int0_right)
+instance int :: add_group {|Auto_tac|}
 instance int :: add_agroup (zadd_commute)
 instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
 instance int :: cring (zmult_commute)