--- a/src/HOL/Number_Theory/UniqueFactorization.thy Sun Mar 07 17:33:01 2010 -0800
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Mon Mar 08 09:38:58 2010 +0100
@@ -295,7 +295,7 @@
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]
@@ -312,7 +312,7 @@
"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]
@@ -636,7 +636,7 @@
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)]
@@ -657,7 +657,7 @@
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: