src/HOL/Real.thy
changeset 58042 ffa9e39763e3
parent 58040 9a867afaab5a
child 58055 625bdd5c70b2
     1.1 --- a/src/HOL/Real.thy	Mon Aug 25 16:06:41 2014 +0200
     1.2 +++ b/src/HOL/Real.thy	Mon Aug 25 14:24:05 2014 +0200
     1.3 @@ -1000,13 +1000,24 @@
     1.4  where
     1.5    "real_of_rat \<equiv> of_rat"
     1.6  
     1.7 -consts
     1.8 -  (*overloaded constant for injecting other types into "real"*)
     1.9 -  real :: "'a => real"
    1.10 +class real_of =
    1.11 +  fixes real :: "'a \<Rightarrow> real"
    1.12 +
    1.13 +instantiation nat :: real_of
    1.14 +begin
    1.15 +
    1.16 +definition real_nat :: "nat \<Rightarrow> real" where real_of_nat_def [code_unfold]: "real \<equiv> of_nat" 
    1.17  
    1.18 -defs (overloaded)
    1.19 -  real_of_nat_def [code_unfold]: "real == real_of_nat"
    1.20 -  real_of_int_def [code_unfold]: "real == real_of_int"
    1.21 +instance ..
    1.22 +end
    1.23 +
    1.24 +instantiation int :: real_of
    1.25 +begin
    1.26 +
    1.27 +definition real_int :: "int \<Rightarrow> real" where real_of_int_def [code_unfold]: "real \<equiv> of_int" 
    1.28 +
    1.29 +instance ..
    1.30 +end
    1.31  
    1.32  declare [[coercion_enabled]]
    1.33  declare [[coercion "real::nat\<Rightarrow>real"]]