src/HOL/Divides.thy

   apply (auto simp add: pos_imp_zdiv_nonneg_iff)
   apply (cases "y = 0")
   apply auto
 done
 
-declare TransferMorphism_nat_int [transfer add return:
+declare transfer_morphism_nat_int [transfer add return:
   transfer_nat_int_functions
   transfer_nat_int_function_closures
 ]
 
 lemma transfer_int_nat_functions:

 lemma transfer_int_nat_function_closures:
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x div y)"
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x mod y)"
   by (simp_all only: is_nat_def transfer_nat_int_function_closures)
 
-declare TransferMorphism_int_nat [transfer add return:
+declare transfer_morphism_int_nat [transfer add return:
   transfer_int_nat_functions
   transfer_int_nat_function_closures
 ]
 
 text{*Suggested by Matthias Daum*}