src/HOL/SetInterval.thy
changeset 35644 d20cf282342e
parent 35580 0f74806cab22
child 35828 46cfc4b8112e
     1.1 --- a/src/HOL/SetInterval.thy	Sun Mar 07 17:33:01 2010 -0800
     1.2 +++ b/src/HOL/SetInterval.thy	Mon Mar 08 09:38:58 2010 +0100
     1.3 @@ -1228,7 +1228,7 @@
     1.4      "x >= 0 \<Longrightarrow> nat_set {x..y}"
     1.5    by (simp add: nat_set_def)
     1.6  
     1.7 -declare TransferMorphism_nat_int[transfer add
     1.8 +declare transfer_morphism_nat_int[transfer add
     1.9    return: transfer_nat_int_set_functions
    1.10      transfer_nat_int_set_function_closures
    1.11  ]
    1.12 @@ -1244,7 +1244,7 @@
    1.13      "is_nat x \<Longrightarrow> nat_set {x..y}"
    1.14    by (simp only: transfer_nat_int_set_function_closures is_nat_def)
    1.15  
    1.16 -declare TransferMorphism_int_nat[transfer add
    1.17 +declare transfer_morphism_int_nat[transfer add
    1.18    return: transfer_int_nat_set_functions
    1.19      transfer_int_nat_set_function_closures
    1.20  ]