| changeset 63950 | cdc1e59aa513 |
| parent 63762 | 6920b1885eff |
| child 64242 | 93c6f0da5c70 |
--- a/src/HOL/Word/Word.thy Mon Sep 26 07:56:54 2016 +0200 +++ b/src/HOL/Word/Word.thy Mon Sep 26 07:56:54 2016 +0200 @@ -287,7 +287,7 @@ lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1" by (metis bintr_ariths(7)) -instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}" +instantiation word :: (len0) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}" begin lift_definition zero_word :: "'a word" is "0" .