diff -r 96d126844adc -r 65ffe9e910d4 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sat Feb 01 19:10:37 2020 +0100
+++ b/src/HOL/Code_Numeral.thy	Sat Feb 01 19:10:40 2020 +0100
@@ -299,7 +299,8 @@
 instance by (standard; transfer)
   (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
     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)+
+    exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
+    even_mask_div_iff)+
 
 end
 
@@ -995,7 +996,8 @@
 instance by (standard; transfer)
   (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
     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)+
+    exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
+    even_mask_div_iff)+
 
 end