# HG changeset patch
# User paulson
# Date 931434491 -7200
# Node ID 78a2ce8fb8dfb647bb056b493ab9404150c5566b
# Parent  c912740c3545a7d37c964ba2ba05ae608cc4772c
Renaming of theorems from _nat0 to _int0 and _nat1 to _int1

diff -r c912740c3545 -r 78a2ce8fb8df src/HOL/ex/IntRing.thy
--- a/src/HOL/ex/IntRing.thy	Thu Jul 08 13:47:27 1999 +0200
+++ b/src/HOL/ex/IntRing.thy	Thu Jul 08 13:48:11 1999 +0200
@@ -10,7 +10,7 @@
 IntRing = IntRingDefs + Lagrange +
 
 instance int :: add_semigroup (zadd_assoc)
-instance int :: add_monoid (zero_int_def,zadd_nat0,zadd_nat0_right)
+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_agroup (zadd_commute)
 instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)