--- a/src/HOL/Code_Numeral.thy Mon Dec 02 18:29:22 2019 +0100
+++ b/src/HOL/Code_Numeral.thy Mon Dec 02 17:15:16 2019 +0000
@@ -297,8 +297,8 @@
is \<open>drop_bit\<close> .
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
+ (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)+
end
@@ -993,8 +993,8 @@
is \<open>drop_bit\<close> .
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
+ (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)+
end