src/HOL/Library/Float.thy
changeset 41024 ba961a606c67
parent 39161 75849a560c09
child 41528 276078f01ada
     1.1 --- a/src/HOL/Library/Float.thy	Fri Dec 03 15:25:14 2010 +0100
     1.2 +++ b/src/HOL/Library/Float.thy	Mon Dec 06 19:54:48 2010 +0100
     1.3 @@ -21,6 +21,9 @@
     1.4  defs (overloaded)
     1.5    real_of_float_def [code_unfold]: "real == of_float"
     1.6  
     1.7 +declare [[coercion "% x . Float x 0"]]
     1.8 +declare [[coercion "real::float\<Rightarrow>real"]]
     1.9 +
    1.10  primrec mantissa :: "float \<Rightarrow> int" where
    1.11    "mantissa (Float a b) = a"
    1.12