doc-src/TutorialI/Types/document/Numbers.tex

 \rulename{zdiv_zadd1_eq}
 
 \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%
 \end{isabelle}
 \rulename{zdiv_zmult1_eq}