--- a/src/HOL/Integ/Bin.ML Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Integ/Bin.ML Fri Nov 02 17:55:24 2001 +0100
@@ -189,6 +189,12 @@
Addsimps (map (inst "y" "number_of ?v")
[zminus_zless, zminus_zle, zminus_equation]);
+(*Equations and inequations involving 1*)
+Addsimps (map (simplify (simpset()) o inst "x" "1")
+ [zless_zminus, zle_zminus, equation_zminus]);
+Addsimps (map (simplify (simpset()) o inst "y" "1")
+ [zminus_zless, zminus_zle, zminus_equation]);
+
(*Moving negation out of products*)
Addsimps [zmult_zminus, zmult_zminus_right];