changeset 66806 | a4e82b58d833 |
parent 66453 | cc19f7ca2ed6 |
child 66815 | 93c6632ddf44 |
--- a/src/HOL/ex/Word_Type.thy Sun Oct 08 22:28:21 2017 +0200 +++ b/src/HOL/ex/Word_Type.thy Sun Oct 08 22:28:21 2017 +0200 @@ -11,7 +11,7 @@ subsection \<open>Truncating bit representations of numeric types\<close> -class semiring_bits = semiring_div_parity + +class semiring_bits = unique_euclidean_semiring_parity + assumes semiring_bits: "(1 + 2 * a) mod of_nat (2 * n) = 1 + 2 * (a mod of_nat n)" begin