diff -r f9038dd937dd -r 9f22b71e209e src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Thu Feb 08 10:59:30 2024 +0000
+++ b/src/HOL/Code_Numeral.thy	Fri Feb 09 16:43:43 2024 +0000
@@ -349,7 +349,7 @@
 
 instance by (standard; transfer)
   (fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
-    half_div_exp_eq even_double_div_exp_iff even_decr_exp_div_exp_iff even_mod_exp_div_exp_iff
+    half_div_exp_eq even_double_div_exp_iff even_mod_exp_div_exp_iff
     bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     and_rec or_rec xor_rec mask_eq_exp_minus_1
     set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
@@ -1109,7 +1109,7 @@
 
 instance by (standard; transfer)
   (fact bit_induct div_by_0 div_by_1 div_0 even_half_succ_eq
-    half_div_exp_eq even_double_div_exp_iff even_decr_exp_div_exp_iff even_mod_exp_div_exp_iff
+    half_div_exp_eq even_double_div_exp_iff even_mod_exp_div_exp_iff
     bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod
     and_rec or_rec xor_rec mask_eq_exp_minus_1
     set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+