src/HOL/ex/IntRing.thy
changeset 11701 3d51fbf81c17
parent 8936 a1c426541757
child 11868 56db9f3a6b3e
--- a/src/HOL/ex/IntRing.thy	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/ex/IntRing.thy	Fri Oct 05 21:52:39 2001 +0200
@@ -10,7 +10,7 @@
 IntRing = Ring + Lagrange +
 
 instance int :: add_semigroup (zadd_assoc)
-instance int :: add_monoid (IntDef.Zero_def,zadd_int0,zadd_int0_right)
+instance int :: add_monoid (Zero_int_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)