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