diff -r 2b17622e1929 -r 138919f1a135 doc-src/TutorialI/Rules/Forward.thy
--- a/doc-src/TutorialI/Rules/Forward.thy	Wed Jul 11 13:57:01 2001 +0200
+++ b/doc-src/TutorialI/Rules/Forward.thy	Wed Jul 11 14:00:48 2001 +0200
@@ -154,7 +154,7 @@
 *}
 
 lemma relprime_dvd_mult: 
-      "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m";
+      "\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"
 apply (insert gcd_mult_distrib2 [of m k n])
 apply simp
 apply (erule_tac t="m" in ssubst);
@@ -169,11 +169,9 @@
 \rulename{mod_div_equality}
 *};
 
-lemma div_mult_self_is_m: 
-      "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
-apply (insert mod_div_equality [of "m*n" n])
-apply simp
-done
+(*MOVED to Force.thy, which now depends only on Divides.thy
+lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)"
+*)
 
 lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> (k dvd m*n) = (k dvd m)";
 by (blast intro: relprime_dvd_mult dvd_trans)