src/Doc/Tutorial/document/rules.tex

--- a/src/Doc/Tutorial/document/rules.tex	Sun Oct 16 09:31:04 2016 +0200
+++ b/src/Doc/Tutorial/document/rules.tex	Sun Oct 16 09:31:05 2016 +0200
@@ -2175,7 +2175,7 @@
 remainder obey a well-known law: 
 \begin{isabelle}
 (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m
-\rulename{mod_div_equality}
+\rulename{div_mult_mod_eq}
 \end{isabelle}
 
 We refer to this law explicitly in the following proof: 
@@ -2183,7 +2183,7 @@
 \isacommand{lemma}\ div_mult_self_is_m:\ \isanewline
 \ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\
 (m::nat)"\isanewline
-\isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m*n"\ n])\isanewline
+\isacommand{apply}\ (insert\ div_mult_mod_eq\ [of\ "m*n"\ n])\isanewline
 \isacommand{apply}\ (simp)\isanewline
 \isacommand{done}
 \end{isabelle}