src/HOL/Real.thy
changeset 59000 6eb0725503fc
parent 58983 9c390032e4eb
child 59587 8ea7b22525cb
     1.1 --- a/src/HOL/Real.thy	Thu Nov 13 14:40:06 2014 +0100
     1.2 +++ b/src/HOL/Real.thy	Thu Nov 13 17:19:52 2014 +0100
     1.3 @@ -1020,13 +1020,17 @@
     1.4  end
     1.5  
     1.6  declare [[coercion_enabled]]
     1.7 -declare [[coercion "real::nat\<Rightarrow>real"]]
     1.8 -declare [[coercion "real::int\<Rightarrow>real"]]
     1.9 -declare [[coercion "int"]]
    1.10 +
    1.11 +declare [[coercion "of_nat :: nat \<Rightarrow> int"]]
    1.12 +declare [[coercion "real   :: nat \<Rightarrow> real"]]
    1.13 +declare [[coercion "real   :: int \<Rightarrow> real"]]
    1.14 +
    1.15 +(* We do not add rat to the coerced types, this has often unpleasant side effects when writing
    1.16 +inverse (Suc n) which sometimes gets two coercions: of_rat (inverse (of_nat (Suc n))) *)
    1.17  
    1.18  declare [[coercion_map map]]
    1.19 -declare [[coercion_map "% f g h x. g (h (f x))"]]
    1.20 -declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
    1.21 +declare [[coercion_map "\<lambda>f g h x. g (h (f x))"]]
    1.22 +declare [[coercion_map "\<lambda>f g (x,y). (f x, g y)"]]
    1.23  
    1.24  lemma real_eq_of_nat: "real = of_nat"
    1.25    unfolding real_of_nat_def ..