# HG changeset patch # User paulson # Date 961154477 -7200 # Node ID 8e9b7095bf5907be33cf25fe4e7dee14967f76b3 # Parent b8780970d0edcb237de3df9b303329a98a62a563 some missing simprules for integer linear arithmetic diff -r b8780970d0ed -r 8e9b7095bf59 src/HOL/Integ/IntArith.ML --- 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;