src/HOL/Library/Float.thy

 primrec of_float :: "float \<Rightarrow> real" where
   "of_float (Float a b) = real a * pow2 b"
 
 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"
 
 primrec scale :: "float \<Rightarrow> int" where