# HG changeset patch
# User paulson
# Date 978211170 -3600
# Node ID 9bc30e51144ceb83748cdc0892b1858ad62a8896
# Parent  e43e017df8c1a2827dfdd34ab1328d019b414a1b
now #16*(x+y) distributes for nat just as for other numeric types

diff -r e43e017df8c1 -r 9bc30e51144c src/HOL/Integ/nat_bin.ML
--- 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]);
+