new rewrite rules for use by arith_tac to take care of uminus.
authornipkow
Wed, 12 Dec 2001 19:21:54 +0100
changeset 12482 d2848ccc9757
parent 12481 ea5d6da573c5
child 12483 0a01efff43e9
new rewrite rules for use by arith_tac to take care of uminus.
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];