some missing simprules for integer linear arithmetic
authorpaulson
Fri Jun 16 13:21:17 2000 +0200 (2000-06-16)
changeset 90798e9b7095bf59
parent 9078 b8780970d0ed
child 9080 67ca888af420
some missing simprules for integer linear arithmetic
src/HOL/Integ/IntArith.ML
     1.1 --- a/src/HOL/Integ/IntArith.ML	Fri Jun 16 13:19:15 2000 +0200
     1.2 +++ b/src/HOL/Integ/IntArith.ML	Fri Jun 16 13:21:17 2000 +0200
     1.3 @@ -394,7 +394,8 @@
     1.4  		 zadd_zminus_inverse, zadd_zminus_inverse2, 
     1.5  		 zmult_0, zmult_0_right, 
     1.6  		 zmult_1, zmult_1_right, 
     1.7 -		 zmult_minus1, zmult_minus1_right];
     1.8 +		 zmult_minus1, zmult_minus1_right,
     1.9 +		 zminus_zadd_distrib, zminus_zminus];
    1.10  
    1.11  val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
    1.12                 Int_Numeral_Simprocs.cancel_numerals;