# HG changeset patch
# User nipkow
# Date 1236011183 -3600
# Node ID 0db3a35eab010b1138cf4515ef21b389b5816de9
# Parent  1b32021f6d9e14f3d57857f938c5d2643fe47696
name fix

diff -r 1b32021f6d9e -r 0db3a35eab01 NEWS
--- 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
diff -r 1b32021f6d9e -r 0db3a35eab01 doc-src/TutorialI/Types/Numbers.thy
--- 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}
diff -r 1b32021f6d9e -r 0db3a35eab01 doc-src/TutorialI/Types/document/Numbers.tex
--- 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%
diff -r 1b32021f6d9e -r 0db3a35eab01 doc-src/TutorialI/Types/numerics.tex
--- 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}