some missing simprules for integer linear arithmetic
authorpaulson
Fri, 16 Jun 2000 13:21:17 +0200
changeset 9079 8e9b7095bf59
parent 9078 b8780970d0ed
child 9080 67ca888af420
some missing simprules for integer linear arithmetic
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;