diff -r 62d8c6c08fb2 -r 1e19abf373ac src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Jan 14 20:02:55 2024 +0000
+++ b/src/HOL/Library/Word.thy	Sun Jan 14 20:02:58 2024 +0000
@@ -1007,19 +1007,11 @@
   show \<open>mask n = 2 ^ n - (1 :: 'a word)\<close>
     by transfer (simp flip: mask_eq_exp_minus_1)
   show \<open>set_bit n v = v OR push_bit n 1\<close>
-    by transfer (simp add: take_bit_set_bit_eq set_bit_eq_or)
-  show \<open>unset_bit 0 v = 2 * (v div 2)\<close>
-    apply transfer
-    apply (rule bit_eqI)
-    apply (auto simp add: bit_simps simp flip: bit_Suc)
-    done
-  show \<open>unset_bit (Suc n) v = v mod 2 + 2 * unset_bit n (v div 2)\<close>
-    apply transfer
-    apply (rule bit_eqI)
-    apply (auto simp add: bit_simps mod_2_eq_odd even_bit_succ_iff bit_0 simp flip: bit_Suc)
-    done
+    by transfer (simp add: set_bit_eq_or)
+  show \<open>unset_bit n v = (v OR push_bit n 1) XOR push_bit n 1\<close>
+    by transfer (simp add: unset_bit_eq_or_xor)
   show \<open>flip_bit n v = v XOR push_bit n 1\<close>
-    by transfer (simp add: take_bit_flip_bit_eq flip_bit_eq_xor)
+    by transfer (simp add: flip_bit_eq_xor)
   show \<open>push_bit n v = v * 2 ^ n\<close>
     by transfer (simp add: push_bit_eq_mult)
   show \<open>drop_bit n v = v div 2 ^ n\<close>