--- a/src/HOL/Code_Numeral.thy Wed Nov 27 16:54:33 2019 +0000
+++ b/src/HOL/Code_Numeral.thy Sun Dec 01 08:00:59 2019 +0000
@@ -299,7 +299,7 @@
instance by (standard; transfer)
(fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
- 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)+
end
@@ -995,7 +995,7 @@
instance by (standard; transfer)
(fact bit_eq_rec bit_induct push_bit_eq_mult drop_bit_eq_div
bits_div_0 bits_div_by_1 bit_mod_div_trivial even_succ_div_2
- 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)+
end