diff -r 127ba61b2630 -r 7449ff77029e src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Tue Nov 21 19:19:16 2023 +0000 +++ b/src/HOL/Code_Numeral.thy Wed Nov 22 17:50:36 2023 +0000 @@ -352,8 +352,8 @@ bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2 exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq even_mask_div_iff even_mult_exp_div_exp_iff - and_rec or_rec xor_rec mask_eq_exp_minus_1 - set_bit_def bit_unset_bit_iff flip_bit_def bit_not_iff_eq minus_eq_not_minus_1)+ + and_rec or_rec xor_rec mask_eq_exp_minus_1 not_rec + set_bit_def bit_unset_bit_iff flip_bit_def not_rec minus_eq_not_minus_1)+ end