src/HOL/Number_Theory/UniqueFactorization.thy

 
 lemma transfer_nat_int_multiplicity: "p >= 0 \<Longrightarrow> n >= 0 \<Longrightarrow>
   multiplicity (nat p) (nat n) = multiplicity p n"
   by (auto simp add: multiplicity_int_def)
 
-declare TransferMorphism_nat_int[transfer add return: 
+declare transfer_morphism_nat_int[transfer add return: 
   transfer_nat_int_prime_factors transfer_nat_int_prime_factors_closure
   transfer_nat_int_multiplicity]
 
 
 lemma transfer_int_nat_prime_factors:

 
 lemma transfer_int_nat_multiplicity: 
     "multiplicity (int p) (int n) = multiplicity p n"
   by (auto simp add: multiplicity_int_def)
 
-declare TransferMorphism_int_nat[transfer add return: 
+declare transfer_morphism_int_nat[transfer add return: 
   transfer_int_nat_prime_factors transfer_int_nat_prime_factors_closure
   transfer_int_nat_multiplicity]
 
 
 subsection {* Properties of prime factors and multiplicity for nats and ints *}

   "(PROD x : A. int (f x)) >= 0"
   apply (rule setsum_nonneg, auto)
   apply (rule setprod_nonneg, auto)
 done
 
-declare TransferMorphism_nat_int[transfer 
+declare transfer_morphism_nat_int[transfer 
   add return: transfer_nat_int_sum_prod_closure3
   del: transfer_nat_int_sum_prod2 (1)]
 
 lemma multiplicity_setprod_int: "p >= 0 \<Longrightarrow> finite S \<Longrightarrow> 
   (ALL x : S. f x > 0) \<Longrightarrow> 

   apply auto
   apply (rule setsum_cong)
   apply auto
 done
 
-declare TransferMorphism_nat_int[transfer 
+declare transfer_morphism_nat_int[transfer 
   add return: transfer_nat_int_sum_prod2 (1)]
 
 lemma multiplicity_prod_prime_powers_nat:
     "finite S \<Longrightarrow> (ALL p : S. prime (p::nat)) \<Longrightarrow>
        multiplicity p (PROD p : S. p ^ f p) = (if p : S then f p else 0)"