src/HOL/Code_Numeral.thy

   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
-    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
 
 lemma [transfer_rule]:
   "rel_fun (=) (rel_fun pcr_integer pcr_integer) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> int) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> integer)"

   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
-    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
 
 lemma [transfer_rule]:
   "rel_fun (=) (rel_fun pcr_natural pcr_natural) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> nat) (take_bit :: _ \<Rightarrow> _ \<Rightarrow> natural)"