| changeset 64242 | 93c6f0da5c70 |
| parent 61945 | 1135b8de26c3 |
| child 64246 | 15d1ee6e847b |
--- a/src/HOL/Word/Bit_Representation.thy Sun Oct 16 09:31:04 2016 +0200 +++ b/src/HOL/Word/Bit_Representation.thy Sun Oct 16 09:31:05 2016 +0200 @@ -43,7 +43,7 @@ lemma bin_rl_simp [simp]: "bin_rest w BIT bin_last w = w" unfolding bin_rest_def bin_last_def Bit_def - using mod_div_equality [of w 2] + using div_mult_mod_eq [of w 2] by (cases "w mod 2 = 0", simp_all) lemma bin_rest_BIT [simp]: "bin_rest (x BIT b) = x"