src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 61115 3a4400985780
parent 60500 903bb1495239
child 61424 c3658c18b7bc
     1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Sep 04 16:01:58 2015 +0200
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Fri Sep 04 19:22:13 2015 +0200
     1.3 @@ -85,20 +85,23 @@
     1.4      and (OCaml) "Pervasives.sqrt"
     1.5  declare sqrt_def[code del]
     1.6  
     1.7 -definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
     1.8 +context
     1.9 +begin
    1.10 +
    1.11 +qualified definition real_exp :: "real \<Rightarrow> real" where "real_exp = exp"
    1.12  
    1.13  lemma exp_eq_real_exp[code_unfold]: "exp = real_exp"
    1.14    unfolding real_exp_def ..
    1.15  
    1.16 +end
    1.17 +
    1.18  code_printing
    1.19 -  constant real_exp \<rightharpoonup>
    1.20 +  constant Code_Real_Approx_By_Float.real_exp \<rightharpoonup>
    1.21      (SML) "Math.exp"
    1.22      and (OCaml) "Pervasives.exp"
    1.23 -declare real_exp_def[code del]
    1.24 +declare Code_Real_Approx_By_Float.real_exp_def[code del]
    1.25  declare exp_def[code del]
    1.26  
    1.27 -hide_const (open) real_exp
    1.28 -
    1.29  code_printing
    1.30    constant ln \<rightharpoonup>
    1.31      (SML) "Math.ln"
    1.32 @@ -149,7 +152,10 @@
    1.33      (SML) "Real.fromInt"
    1.34      and (OCaml) "Pervasives.float (Big'_int.int'_of'_big'_int (_))"
    1.35  
    1.36 -definition real_of_int :: "int \<Rightarrow> real" where
    1.37 +context
    1.38 +begin
    1.39 +
    1.40 +qualified definition real_of_int :: "int \<Rightarrow> real" where
    1.41    [code_abbrev]: "real_of_int = of_int"
    1.42  
    1.43  lemma [code]:
    1.44 @@ -172,7 +178,7 @@
    1.45    "- numeral k \<equiv> (of_rat (- numeral k) :: real)"
    1.46    by simp
    1.47  
    1.48 -hide_const (open) real_of_int
    1.49 +end
    1.50  
    1.51  code_printing
    1.52    constant Ratreal \<rightharpoonup> (SML)