src/HOL/Nat_Transfer.thy

 
 declare transfer_morphism_int_nat [transfer add
   return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
   cong: setsum_cong setprod_cong]
 
+
+(*belongs to Divides.thy, but slows down dependency discovery*)
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
 end