--- a/src/HOL/Library/Float.thy Thu Dec 29 10:47:55 2011 +0100
+++ b/src/HOL/Library/Float.thy Thu Dec 29 10:47:55 2011 +0100
@@ -45,10 +45,12 @@
instance ..
end
-lemma number_of_float_Float [code_unfold_post]:
+lemma number_of_float_Float:
"number_of k = Float (number_of k) 0"
by (simp add: number_of_float_def number_of_is_id)
+declare number_of_float_Float [symmetric, code_abbrev]
+
lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
unfolding real_of_float_def using of_float.simps .