--- a/NEWS Mon Mar 02 16:54:13 2009 +0100
+++ b/NEWS Mon Mar 02 17:26:23 2009 +0100
@@ -398,6 +398,7 @@
zmod_zadd_right_eq -> mod_add_right_eq
zmod_zadd_self1 -> mod_add_self1
zmod_zadd_self2 -> mod_add_self2
+zmod_zadd1_eq -> mod_add1_eq
zmod_zdiff1_eq -> mod_diff_eq
zmod_zdvd_zmod -> mod_mod_cancel
zmod_zmod_cancel -> mod_mod_cancel
--- a/doc-src/TutorialI/Types/Numbers.thy Mon Mar 02 16:54:13 2009 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy Mon Mar 02 17:26:23 2009 +0100
@@ -147,8 +147,8 @@
@{thm[display] zdiv_zadd1_eq[no_vars]}
\rulename{zdiv_zadd1_eq}
-@{thm[display] zmod_zadd1_eq[no_vars]}
-\rulename{zmod_zadd1_eq}
+@{thm[display] mod_add1_eq[no_vars]}
+\rulename{mod_add1_eq}
@{thm[display] zdiv_zmult1_eq[no_vars]}
\rulename{zdiv_zmult1_eq}
--- 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%
--- a/doc-src/TutorialI/Types/numerics.tex Mon Mar 02 16:54:13 2009 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Mon Mar 02 17:26:23 2009 +0100
@@ -276,7 +276,7 @@
\rulename{zdiv_zadd1_eq}
\par\smallskip
(a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
-\rulename{zmod_zadd1_eq}
+\rulename{mod_add1_eq}
\end{isabelle}
\begin{isabelle}