--- a/src/HOL/Divides.thy Thu May 31 18:16:47 2007 +0200
+++ b/src/HOL/Divides.thy Thu May 31 18:16:50 2007 +0200
@@ -375,18 +375,6 @@
done
-(*Distribution of Factors over Remainders:
-
-Could prove these as in Integ/IntDiv.ML, but we already have
-mod_mult_distrib and mod_mult_distrib2 above!
-
-Goal "(c*a) mod (c*b) = (c::nat) * (a mod b)"
-qed "mod_mult_mult1";
-
-Goal "(a*c) mod (b*c) = (a mod b) * (c::nat)";
-qed "mod_mult_mult2";
- ***)
-
subsection{*Further Facts about Quotient and Remainder*}
lemma div_1 [simp]: "m div Suc 0 = m"