--- a/src/HOL/Int.thy Mon Mar 17 18:36:04 2008 +0100
+++ b/src/HOL/Int.thy Mon Mar 17 18:37:00 2008 +0100
@@ -1911,10 +1911,6 @@
lemmas zdiff_zmult_distrib = left_diff_distrib [of "z1::int" "z2" "w", standard]
lemmas zdiff_zmult_distrib2 = right_diff_distrib [of "w::int" "z1" "z2", standard]
-lemmas int_distrib =
- zadd_zmult_distrib zadd_zmult_distrib2
- zdiff_zmult_distrib zdiff_zmult_distrib2
-
lemmas zmult_1 = mult_1_left [of "z::int", standard]
lemmas zmult_1_right = mult_1_right [of "z::int", standard]