doc-src/TutorialI/Types/document/Numbers.tex
changeset 30200 0db3a35eab01
parent 29297 62e0f892e525
child 30224 79136ce06bdb
--- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon Mar 02 16:54:13 2009 +0100
+++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon Mar 02 17:26:23 2009 +0100
@@ -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{zmod_zadd1_eq}
+\rulename{mod_add1_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%