new rewrite rules for use by arith_tac to take care of uminus.
authornipkow
Wed Dec 12 19:21:54 2001 +0100 (2001-12-12)
changeset 12482d2848ccc9757
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
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Dec 12 19:21:02 2001 +0100
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Wed Dec 12 19:21:54 2001 +0100
     1.3 @@ -410,8 +410,8 @@
     1.4       zminus_0, zadd_0, zadd_0_right, zdiff_def,
     1.5       zadd_zminus_inverse, zadd_zminus_inverse2, 
     1.6       zmult_0, zmult_0_right, 
     1.7 -     zmult_1, zmult_1_right, 
     1.8 -     zmult_minus1, zmult_minus1_right,
     1.9 +     zmult_1, zmult_1_right,
    1.10 +     zmult_zminus, zmult_zminus_right,
    1.11       zminus_zadd_distrib, zminus_zminus, zmult_assoc,
    1.12       int_0, int_1, zadd_int RS sym, int_Suc];
    1.13