doc-src/TutorialI/Types/document/Numbers.tex
changeset 30224 79136ce06bdb
parent 30200 0db3a35eab01
child 30242 aea5d7fa7ef5
     1.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -244,7 +244,7 @@
     1.4  \begin{isabelle}%
     1.5  a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c%
     1.6  \end{isabelle}
     1.7 -\rulename{mod_mult1_eq}
     1.8 +\rulename{mod_mult_right_eq}
     1.9  
    1.10  \begin{isabelle}%
    1.11  a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
    1.12 @@ -318,7 +318,7 @@
    1.13  \begin{isabelle}%
    1.14  {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c%
    1.15  \end{isabelle}
    1.16 -\rulename{mod_add1_eq}
    1.17 +\rulename{mod_add_eq}
    1.18  
    1.19  \begin{isabelle}%
    1.20  a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c%