src/HOL/Code_Numeral.thy
changeset 79018 7449ff77029e
parent 79016 74440d820ba5
child 79031 4596a14d9a95
--- 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