now #16*(x+y) distributes for nat just as for other numeric types

--- a/src/HOL/Integ/nat_bin.ML	Sat Dec 30 22:17:34 2000 +0100
+++ b/src/HOL/Integ/nat_bin.ML	Sat Dec 30 22:19:30 2000 +0100
@@ -544,3 +544,9 @@
                           nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
 by (arith_tac 1);
 qed "nat_abs_mult_distrib";
+
+(*Distributive laws for literals*)
+Addsimps (map (inst "k" "number_of ?v")
+	  [add_mult_distrib, add_mult_distrib2,
+	   diff_mult_distrib, diff_mult_distrib2]);
+