--- a/src/Doc/Tutorial/Rules/Forward.thy	Wed Jun 19 12:13:16 2024 +0200
+++ b/src/Doc/Tutorial/Rules/Forward.thy	Thu Jun 20 14:28:46 2024 +0000
@@ -187,10 +187,6 @@
 \rulename{div_mult_mod_eq}
 \<close>
 
-(*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 (auto intro: relprime_dvd_mult elim: dvdE)