src/HOL/Code_Numeral.thy
changeset 79489 1e19abf373ac
parent 79488 62d8c6c08fb2
child 79531 22a137a6de44
--- a/src/HOL/Code_Numeral.thy	Sun Jan 14 20:02:55 2024 +0000
+++ b/src/HOL/Code_Numeral.thy	Sun Jan 14 20:02:58 2024 +0000
@@ -353,7 +353,7 @@
     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 unset_bit_0 unset_bit_Suc flip_bit_def not_eq_complement)+
+    set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor not_eq_complement)+
 
 end
 
@@ -1111,7 +1111,7 @@
     bits_div_0 bits_div_by_0 bits_div_by_1 even_half_succ_eq
     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 unset_bit_0 unset_bit_Suc flip_bit_def)+
+    mask_eq_exp_minus_1 set_bit_eq_or unset_bit_eq_or_xor flip_bit_eq_xor)+
 
 end