# HG changeset patch
# User wenzelm
# Date 973880317 -3600
# Node ID 226d474e644df8dbf66543bcae56281e908a4cf2
# Parent  60ddd5fdf93b893eb52011659837e84016374135
int_distrib;

diff -r 60ddd5fdf93b -r 226d474e644d src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Fri Nov 10 19:18:14 2000 +0100
+++ b/src/HOL/Integ/IntDef.ML	Fri Nov 10 19:18:37 2000 +0100
@@ -319,6 +319,9 @@
 by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
 qed "zdiff_zmult_distrib2";
 
+bind_thms ("int_distrib",
+  [zadd_zmult_distrib, zadd_zmult_distrib2, zdiff_zmult_distrib, zdiff_zmult_distrib2]);
+
 Goalw [int_def] "(int m) * (int n) = int (m * n)";
 by (simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_int";