diff -r eed4ca224c9c -r 74a4776f7a22 src/HOL/Code_Numeral.thy --- a/src/HOL/Code_Numeral.thy Sat Nov 18 19:23:56 2023 +0100 +++ b/src/HOL/Code_Numeral.thy Sun Nov 19 15:45:22 2023 +0000 @@ -352,7 +352,7 @@ 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 - bit_and_iff bit_or_iff bit_xor_iff mask_eq_exp_minus_1 + 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)+ end @@ -1110,7 +1110,7 @@ (fact bit_eq_rec bits_induct bit_iff_odd push_bit_eq_mult drop_bit_eq_div take_bit_eq_mod 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 bit_and_iff bit_or_iff bit_xor_iff + 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)+ end