# HG changeset patch
# User wenzelm
# Date 973880294 -3600
# Node ID 60ddd5fdf93b893eb52011659837e84016374135
# Parent  088aa7bd3154a15f8326d8dd09ec2407878f22d5
nat_distrib;

diff -r 088aa7bd3154 -r 60ddd5fdf93b src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Fri Nov 10 19:17:46 2000 +0100
+++ b/src/HOL/Nat.ML	Fri Nov 10 19:18:14 2000 +0100
@@ -610,6 +610,9 @@
 qed "diff_mult_distrib2" ;
 (*NOT added as rewrites, since sometimes they are used from right-to-left*)
 
+bind_thms ("nat_distrib",
+  [add_mult_distrib, add_mult_distrib2, diff_mult_distrib, diff_mult_distrib2]);
+
 
 (*** Monotonicity of Multiplication ***)