src/HOL/Library/Float.thy

--- a/src/HOL/Library/Float.thy	Fri Dec 03 15:25:14 2010 +0100
+++ b/src/HOL/Library/Float.thy	Mon Dec 06 19:54:48 2010 +0100
@@ -21,6 +21,9 @@
 defs (overloaded)
   real_of_float_def [code_unfold]: "real == of_float"
 
+declare [[coercion "% x . Float x 0"]]
+declare [[coercion "real::float\<Rightarrow>real"]]
+
 primrec mantissa :: "float \<Rightarrow> int" where
   "mantissa (Float a b) = a"