doc-src/TutorialI/Types/numerics.tex
changeset 30224 79136ce06bdb
parent 30200 0db3a35eab01
child 30242 aea5d7fa7ef5
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4  a\ *\ b\ div\ c\ =\ a\ *\ (b\ div\ c)\ +\ a\ *\ (b\ mod\ c)\ div\ c%
     1.5  \rulename{div_mult1_eq}\isanewline
     1.6  a\ *\ b\ mod\ c\ =\ a\ *\ (b\ mod\ c)\ mod\ c%
     1.7 -\rulename{mod_mult1_eq}\isanewline
     1.8 +\rulename{mod_mult_right_eq}\isanewline
     1.9  a\ div\ (b*c)\ =\ a\ div\ b\ div\ c%
    1.10  \rulename{div_mult2_eq}\isanewline
    1.11  a\ mod\ (b*c)\ =\ b * (a\ div\ b\ mod\ c)\ +\ a\ mod\ b%
    1.12 @@ -276,7 +276,7 @@
    1.13  \rulename{zdiv_zadd1_eq}
    1.14  \par\smallskip
    1.15  (a\ +\ b)\ mod\ c\ =\ (a\ mod\ c\ +\ b\ mod\ c)\ mod\ c%
    1.16 -\rulename{mod_add1_eq}
    1.17 +\rulename{mod_add_eq}
    1.18  \end{isabelle}
    1.19  
    1.20  \begin{isabelle}