# HG changeset patch
# User immler
# Date 1456484022 -3600
# Node ID c7d6f4dded193e980fda05b69f0d51eaffb43693
# Parent  f1b0908028cfed1a6f5967e6fff2d0a806b64302
compute_real_of_float has not been used as code equation

diff -r f1b0908028cf -r c7d6f4dded19 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Thu Feb 25 20:35:05 2016 +0100
+++ b/src/HOL/Library/Float.thy	Fri Feb 26 11:53:42 2016 +0100
@@ -171,12 +171,12 @@
   by simp
 declare Float.rep_eq[simp]
 
+code_datatype Float
+
 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: powr_int)
 
-code_datatype Float
-
 
 subsection \<open>Arithmetic operations on floating point numbers\<close>