int_distrib;

--- 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";