src/HOL/Integ/Bin.ML

--- a/src/HOL/Integ/Bin.ML	Wed May 03 18:30:29 2000 +0200
+++ b/src/HOL/Integ/Bin.ML	Wed May 03 18:33:28 2000 +0200
@@ -265,6 +265,13 @@
 by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
 qed "zmult_2_right";
 
+(*Negation of a coefficient*)
+Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";
+by (simp_tac (simpset_of Int.thy addsimps [number_of_minus, zmult_zminus]) 1);
+qed "zminus_number_of_zmult";
+
+Addsimps [zminus_number_of_zmult];
+
 
 (** Inequality reasoning **)