--- a/src/HOL/Code_Numeral.thy Wed Feb 21 10:46:22 2024 +0000
+++ b/src/HOL/Code_Numeral.thy Wed Feb 21 16:19:36 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_mod_exp_div_exp_iff
+ half_div_exp_eq even_double_div_exp_iff bits_mod_div_trivial
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_mod_exp_div_exp_iff
+ half_div_exp_eq even_double_div_exp_iff bits_mod_div_trivial
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)+