--- 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)