| changeset 9079 | 8e9b7095bf59 |
| parent 9063 | 0d7628966069 |
| child 9214 | 9454f30eacc7 |
--- a/src/HOL/Integ/IntArith.ML Fri Jun 16 13:19:15 2000 +0200 +++ b/src/HOL/Integ/IntArith.ML Fri Jun 16 13:21:17 2000 +0200 @@ -394,7 +394,8 @@ zadd_zminus_inverse, zadd_zminus_inverse2, zmult_0, zmult_0_right, zmult_1, zmult_1_right, - zmult_minus1, zmult_minus1_right]; + zmult_minus1, zmult_minus1_right, + zminus_zadd_distrib, zminus_zminus]; val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@ Int_Numeral_Simprocs.cancel_numerals;