changeset 76247 | e19d4c1c48ce |
parent 76143 | e278bf6430cf |
child 76248 | da4e57d30579 |
76246:c9ea813f92f2 | 76247:e19d4c1c48ce |
---|---|
1 (* Author: Florian Haftmann, TU Muenchen |
1 (* Author: Florian Haftmann, TU Muenchen |
2 *) |
2 *) |
3 |
3 |
4 subsection \<open>Rounded division: modulus centered towars zero.\<close> |
4 subsection \<open>Rounded division: modulus centered towards zero.\<close> |
5 |
5 |
6 theory Rounded_Division |
6 theory Rounded_Division |
7 imports Main |
7 imports Main |
8 begin |
8 begin |
9 |
9 |