# HG changeset patch
# User wenzelm
# Date 1180628210 -7200
# Node ID b9853c187a1e634ce5ad15d78577b7f36d7af8c8
# Parent  cd928fd965a8efcd09c1ef069f2444b780f27926
removed dead code;

diff -r cd928fd965a8 -r b9853c187a1e src/HOL/Divides.thy
--- 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"