--- a/doc-src/TutorialI/Types/document/Numbers.tex Tue Mar 03 12:14:52 2009 +1100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex Tue Mar 03 17:05:18 2009 +0100
@@ -244,7 +244,7 @@
\begin{isabelle}%
a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c%
\end{isabelle}
-\rulename{mod_mult1_eq}
+\rulename{mod_mult_right_eq}
\begin{isabelle}%
a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
@@ -318,7 +318,7 @@
\begin{isabelle}%
{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c%
\end{isabelle}
-\rulename{mod_add1_eq}
+\rulename{mod_add_eq}
\begin{isabelle}%
a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c%