equal
deleted
inserted
replaced
1651 qed |
1651 qed |
1652 |
1652 |
1653 |
1653 |
1654 |
1654 |
1655 subsection \<open>Division on \<^typ>\<open>int\<close>\<close> |
1655 subsection \<open>Division on \<^typ>\<open>int\<close>\<close> |
|
1656 |
|
1657 text \<open> |
|
1658 The following specification of integer division rounds towards minus infinity |
|
1659 and is advocated by Donald Knuth. See \cite{leijen01} for an overview and |
|
1660 terminology of different possibilities to specify integer division; |
|
1661 there division rounding towards minus infinitiy is named ``F-division''. |
|
1662 \<close> |
1656 |
1663 |
1657 subsubsection \<open>Basic instantiation\<close> |
1664 subsubsection \<open>Basic instantiation\<close> |
1658 |
1665 |
1659 instantiation int :: "{normalization_semidom, idom_modulo}" |
1666 instantiation int :: "{normalization_semidom, idom_modulo}" |
1660 begin |
1667 begin |