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 +
```