--- a/src/HOL/ex/Word.thy Fri May 08 06:26:27 2020 +0000
+++ b/src/HOL/ex/Word.thy Fri May 08 06:26:28 2020 +0000
@@ -592,7 +592,8 @@
show \<open>(1 + a) div 2 = a div 2\<close>
if \<open>even a\<close>
for a :: \<open>'a word\<close>
- using that by transfer (auto dest: le_Suc_ex simp add: take_bit_Suc)
+ using that by transfer
+ (auto dest: le_Suc_ex simp add: mod_2_eq_odd take_bit_Suc elim!: evenE)
show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
for m n :: nat
by transfer (simp, simp add: exp_div_exp_eq)