# HG changeset patch
# User paulson
# Date 907259405 -7200
# Node ID b6456ccd9e3e329bd8a4cce39fb4c85133f6ce3d
# Parent  34b3366b83ac50dec77ca07f1dcee10af58325b0
revised for new treatment of integers

diff -r 34b3366b83ac -r b6456ccd9e3e src/HOL/ex/BinEx.ML
--- a/src/HOL/ex/BinEx.ML	Thu Oct 01 18:29:53 1998 +0200
+++ b/src/HOL/ex/BinEx.ML	Thu Oct 01 18:30:05 1998 +0200
@@ -83,6 +83,45 @@
 result();
 
 
+(** Testing the cancellation of complementary terms **)
+
+Goal "y + (x + -x) = int 0 + y";
+by (Simp_tac 1);
+result();
+
+Goal "y + (-x + (- y + x)) = int 0";
+by (Simp_tac 1);
+result();
+
+Goal "-x + (y + (- y + x)) = int 0";
+by (Simp_tac 1);
+result();
+
+Goal "x + (x + (- x + (- x + (- y + - z)))) = int 0 - y - z";
+by (Simp_tac 1);
+result();
+
+Goal "x + x - x - x - y - z = int 0 - y - z";
+by (Simp_tac 1);
+result();
+
+Goal "x + y + z - (x + z) = y - int 0";
+by (Simp_tac 1);
+result();
+
+Goal "x+(y+(y+(y+ (-x + -x)))) = int 0 + y - x + y + y";
+by (Simp_tac 1);
+result();
+
+Goal "x+(y+(y+(y+ (-y + -x)))) = y + int 0 + y";
+by (Simp_tac 1);
+result();
+
+Goal "x + y - x + z - x - y - z + x < int 1";
+by (Simp_tac 1);
+result();
+
+
 Addsimps normal.intrs;
 
 Goal "(w BIT b): normal ==> (w BIT b BIT c): normal";
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)
diff -r 34b3366b83ac -r b6456ccd9e3e src/HOL/ex/IntRingDefs.ML
--- a/src/HOL/ex/IntRingDefs.ML	Thu Oct 01 18:29:53 1998 +0200
+++ b/src/HOL/ex/IntRingDefs.ML	Thu Oct 01 18:30:05 1998 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Integ/IntRingDefs.thy
+(*  Title:      HOL/ex/IntRingDefs.thy
     ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel
     Copyright   1996 TU Muenchen
diff -r 34b3366b83ac -r b6456ccd9e3e src/HOL/ex/IntRingDefs.thy
--- a/src/HOL/ex/IntRingDefs.thy	Thu Oct 01 18:29:53 1998 +0200
+++ b/src/HOL/ex/IntRingDefs.thy	Thu Oct 01 18:30:05 1998 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Integ/IntRingDefs.thy
+(*  Title:      HOL/ex/IntRingDefs.thy
     ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel
     Copyright   1996 TU Muenchen
@@ -10,6 +10,6 @@
 IntRingDefs = Main + Ring +
 
 instance int :: zero
-defs zero_int_def "zero::int == #0"
+defs zero_int_def "zero::int == int 0"
 
 end