src/HOL/Number_Theory/Primes.thy
changeset 35644 d20cf282342e
parent 33946 fcc20072df9a
child 37294 a2a8216999a2
     1.1 --- a/src/HOL/Number_Theory/Primes.thy	Sun Mar 07 17:33:01 2010 -0800
     1.2 +++ b/src/HOL/Number_Theory/Primes.thy	Mon Mar 08 09:38:58 2010 +0100
     1.3 @@ -73,14 +73,14 @@
     1.4    unfolding gcd_int_def lcm_int_def prime_int_def
     1.5    by auto
     1.6  
     1.7 -declare TransferMorphism_nat_int[transfer add return:
     1.8 +declare transfer_morphism_nat_int[transfer add return:
     1.9      transfer_nat_int_prime]
    1.10  
    1.11  lemma transfer_int_nat_prime:
    1.12    "prime (int x) = prime x"
    1.13    by (unfold gcd_int_def lcm_int_def prime_int_def, auto)
    1.14  
    1.15 -declare TransferMorphism_int_nat[transfer add return:
    1.16 +declare transfer_morphism_int_nat[transfer add return:
    1.17      transfer_int_nat_prime]
    1.18  
    1.19