src/HOL/Number_Theory/UniqueFactorization.thy
changeset 35644 d20cf282342e
parent 35416 d8d7d1b785af
child 36903 489c1fbbb028
--- 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: