changeset 64242 | 93c6f0da5c70 |
parent 57514 | bdc2c6b40bf2 |
child 68635 | 8094b853a92f |
--- a/src/Doc/Tutorial/document/numerics.tex Sun Oct 16 09:31:04 2016 +0200 +++ b/src/Doc/Tutorial/document/numerics.tex Sun Oct 16 09:31:05 2016 +0200 @@ -143,7 +143,7 @@ m\ mod\ n\ =\ (if\ m\ <\ n\ then\ m\ else\ (m\ -\ n)\ mod\ n) \rulename{mod_if}\isanewline m\ div\ n\ *\ n\ +\ m\ mod\ n\ =\ m% -\rulenamedx{mod_div_equality} +\rulenamedx{div_mult_mod_eq} \end{isabelle} Many less obvious facts about quotient and remainder are also provided.