src/HOL/Integ/int_arith1.ML
changeset 12482 d2848ccc9757
parent 12018 ec054019c910
child 12975 d796a2fd6c69
     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