src/HOL/GCD.thy
changeset 35644 d20cf282342e
parent 35368 19b340c3f1ff
child 35726 059d2f7b979f
     1.1 --- a/src/HOL/GCD.thy	Sun Mar 07 17:33:01 2010 -0800
     1.2 +++ b/src/HOL/GCD.thy	Mon Mar 08 09:38:58 2010 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4    "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
     1.5    by (auto simp add: gcd_int_def lcm_int_def)
     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_gcd transfer_nat_int_gcd_closures]
    1.10  
    1.11  lemma transfer_int_nat_gcd:
    1.12 @@ -112,7 +112,7 @@
    1.13    "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
    1.14    by (auto simp add: gcd_int_def lcm_int_def)
    1.15  
    1.16 -declare TransferMorphism_int_nat[transfer add return:
    1.17 +declare transfer_morphism_int_nat[transfer add return:
    1.18      transfer_int_nat_gcd transfer_int_nat_gcd_closures]
    1.19  
    1.20