src/HOL/Code_Numeral.thy
changeset 79008 74a4776f7a22
parent 78955 74147aa81dbb
child 79016 74440d820ba5
--- 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