src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 47108 2a1953f0d20d
parent 46530 d5d14046686f
child 51143 0a2371e7ced3
     1.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -129,9 +129,23 @@
     1.4  lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
     1.5    unfolding real_of_int_def ..
     1.6  
     1.7 -hide_const (open) real_of_int
     1.8 +lemma [code_unfold del]:
     1.9 +  "0 \<equiv> (of_rat 0 :: real)"
    1.10 +  by simp
    1.11 +
    1.12 +lemma [code_unfold del]:
    1.13 +  "1 \<equiv> (of_rat 1 :: real)"
    1.14 +  by simp
    1.15  
    1.16 -declare number_of_real_code [code_unfold del]
    1.17 +lemma [code_unfold del]:
    1.18 +  "numeral k \<equiv> (of_rat (numeral k) :: real)"
    1.19 +  by simp
    1.20 +
    1.21 +lemma [code_unfold del]:
    1.22 +  "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
    1.23 +  by simp
    1.24 +
    1.25 +hide_const (open) real_of_int
    1.26  
    1.27  notepad
    1.28  begin