# HG changeset patch
# User hoelzl
# Date 1335444170 -7200
# Node ID 3357688660ffeb1e31b03e8dc36aa87ed57dd9f9
# Parent  5a10e24fe7abd1de7bd28160f46e1c5e725c2d1f
add code equation for real_of_float

diff -r 5a10e24fe7ab -r 3357688660ff src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Apr 26 14:11:13 2012 +0200
+++ b/src/HOL/Library/Float.thy	Thu Apr 26 14:42:50 2012 +0200
@@ -130,6 +130,10 @@
 lift_definition Float :: "int \<Rightarrow> int \<Rightarrow> float" is "\<lambda>(m::int) (e::int). m * 2 powr e" by simp
 declare Float.rep_eq[simp]
 
+lemma compute_real_of_float[code]:
+  "real_of_float (Float m e) = (if e \<ge> 0 then m * 2 ^ nat e else m / 2 ^ (nat (-e)))"
+by (simp add: real_of_float_def[symmetric] powr_int)
+
 code_datatype Float
 
 subsection {* Arithmetic operations on floating point numbers *}