src/Doc/Tutorial/document/numerics.tex
changeset 64242 93c6f0da5c70
parent 57514 bdc2c6b40bf2
child 68635 8094b853a92f
--- a/src/Doc/Tutorial/document/numerics.tex	Sun Oct 16 09:31:04 2016 +0200
+++ b/src/Doc/Tutorial/document/numerics.tex	Sun Oct 16 09:31:05 2016 +0200
@@ -143,7 +143,7 @@
 m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n)
 \rulename{mod_if}\isanewline
 m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m%
-\rulenamedx{mod_div_equality}
+\rulenamedx{div_mult_mod_eq}
 \end{isabelle}
 
 Many less obvious facts about quotient and remainder are also provided.