src/HOL/Library/Code_Real_Approx_By_Float.thy
changeset 47108 2a1953f0d20d
parent 46530 d5d14046686f
child 51143 0a2371e7ced3
--- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sun Mar 25 20:15:39 2012 +0200
@@ -129,9 +129,23 @@
 lemma of_int_eq_real_of_int[code_unfold]: "of_int = real_of_int"
   unfolding real_of_int_def ..
 
-hide_const (open) real_of_int
+lemma [code_unfold del]:
+  "0 \<equiv> (of_rat 0 :: real)"
+  by simp
+
+lemma [code_unfold del]:
+  "1 \<equiv> (of_rat 1 :: real)"
+  by simp
 
-declare number_of_real_code [code_unfold del]
+lemma [code_unfold del]:
+  "numeral k \<equiv> (of_rat (numeral k) :: real)"
+  by simp
+
+lemma [code_unfold del]:
+  "neg_numeral k \<equiv> (of_rat (neg_numeral k) :: real)"
+  by simp
+
+hide_const (open) real_of_int
 
 notepad
 begin