# HG changeset patch
# User nipkow
# Date 1008181314 -3600
# Node ID d2848ccc9757f5852aeb45ce4dc7e2b086613917
# Parent  ea5d6da573c540fba6fa1584b636b740a1d6dad6
new rewrite rules for use by arith_tac to take care of uminus.

diff -r ea5d6da573c5 -r d2848ccc9757 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Wed Dec 12 19:21:02 2001 +0100
+++ b/src/HOL/Integ/int_arith1.ML	Wed Dec 12 19:21:54 2001 +0100
@@ -410,8 +410,8 @@
      zminus_0, zadd_0, zadd_0_right, zdiff_def,
      zadd_zminus_inverse, zadd_zminus_inverse2, 
      zmult_0, zmult_0_right, 
-     zmult_1, zmult_1_right, 
-     zmult_minus1, zmult_minus1_right,
+     zmult_1, zmult_1_right,
+     zmult_zminus, zmult_zminus_right,
      zminus_zadd_distrib, zminus_zminus, zmult_assoc,
      int_0, int_1, zadd_int RS sym, int_Suc];