src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 51143 0a2371e7ced3
parent 47108 2a1953f0d20d
child 51542 738598beeb26
     1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Feb 15 08:31:30 2013 +0100
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Feb 15 08:31:31 2013 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (* Authors: Florian Haftmann, Johannes Hölzl, Tobias Nipkow *)
     1.5  
     1.6  theory Code_Real_Approx_By_Float
     1.7 -imports Complex_Main "~~/src/HOL/Library/Code_Integer"
     1.8 +imports Complex_Main "~~/src/HOL/Library/Code_Target_Int"
     1.9  begin
    1.10  
    1.11  text{* \textbf{WARNING} This theory implements mathematical reals by machine
    1.12 @@ -119,15 +119,19 @@
    1.13    (OCaml "Pervasives.asin")
    1.14  declare arcsin_def[code del]
    1.15  
    1.16 -definition real_of_int :: "int \<Rightarrow> real" where
    1.17 -  "real_of_int \<equiv> of_int"
    1.18 +definition real_of_integer :: "integer \<Rightarrow> real" where
    1.19 +  "real_of_integer = of_int \<circ> int_of_integer"
    1.20  
    1.21 -code_const real_of_int
    1.22 +code_const real_of_integer
    1.23    (SML "Real.fromInt")
    1.24    (OCaml "Pervasives.float (Big'_int.int'_of'_big'_int (_))")
    1.25  
    1.26 -lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
    1.27 -  unfolding real_of_int_def ..
    1.28 +definition real_of_int :: "int \<Rightarrow> real" where
    1.29 +  [code_abbrev]: "real_of_int = of_int"
    1.30 +
    1.31 +lemma [code]:
    1.32 +  "real_of_int = real_of_integer \<circ> integer_of_int"
    1.33 +  by (simp add: fun_eq_iff real_of_integer_def real_of_int_def)
    1.34  
    1.35  lemma [code_unfold del]:
    1.36    "0 \<equiv> (of_rat 0 :: real)"
    1.37 @@ -155,3 +159,4 @@
    1.38  end
    1.39  
    1.40  end
    1.41 +