diff -r 47272fac86d8 -r 62d8c6c08fb2 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sun Jan 14 20:55:58 2024 +0100
+++ b/src/HOL/Bit_Operations.thy	Sun Jan 14 20:02:55 2024 +0000
@@ -17,7 +17,7 @@
   assumes bits_div_0 [simp]: \<open>0 div a = 0\<close>
     and bits_div_by_0 [simp]: \<open>a div 0 = 0\<close>
     and bits_div_by_1 [simp]: \<open>a div 1 = a\<close>
-    and even_succ_div_2 [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
+    and even_half_succ_eq [simp]: \<open>even a \<Longrightarrow> (1 + a) div 2 = a div 2\<close>
     and even_mask_div_iff: \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
     and exp_div_exp_eq: \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
     and div_exp_eq: \<open>a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)\<close>
@@ -37,7 +37,7 @@
 
 lemma bits_1_div_2 [simp]:
   \<open>1 div 2 = 0\<close>
-  using even_succ_div_2 [of 0] by simp
+  using even_half_succ_eq [of 0] by simp
 
 lemma bits_1_div_exp [simp]:
   \<open>1 div 2 ^ n = of_bool (n = 0)\<close>