--- a/src/HOL/ex/Word.thy Tue Jan 28 20:26:23 2020 +0100
+++ b/src/HOL/ex/Word.thy Sat Feb 01 19:10:37 2020 +0100
@@ -546,11 +546,11 @@
n < LENGTH('a) \<and> odd (a div 2 ^ (n - m)))\<close> for a :: \<open>'a::len word\<close>
by transfer
(auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff,
- simp_all flip: push_bit_eq_mult add: bit_push_bit_eq_int)
+ simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int)
-(*lemma even_range_div_iff_word:
+(*lemma even_mask_div_iff_word:
\<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a::len word) \<or> m \<le> n\<close>
- by transfer (auto simp add: take_bit_of_range even_range_div_iff)*)
+ by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)*)
instance word :: (len) semiring_bits
proof