src/Doc/Tutorial/Rules/Forward.thy

--- a/src/Doc/Tutorial/Rules/Forward.thy	Sun Oct 16 09:31:04 2016 +0200
+++ b/src/Doc/Tutorial/Rules/Forward.thy	Sun Oct 16 09:31:05 2016 +0200
@@ -183,8 +183,8 @@
 
 Another example of "insert"
 
-@{thm[display] mod_div_equality}
-\rulename{mod_div_equality}
+@{thm[display] div_mult_mod_eq}
+\rulename{div_mult_mod_eq}
 *}
 
 (*MOVED to Force.thy, which now depends only on Divides.thy