1.1 --- a/src/HOL/Library/Float.thy	Fri Jun 05 14:07:54 2009 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Thu Jun 04 17:55:47 2009 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4    "scale (Float a b) = b"
     1.5  
     1.6  instantiation float :: zero begin
     1.7 -definition zero_float where "0 = Float 0 0" 
     1.8 +definition zero_float where "0 = Float 0 0"
     1.9  instance ..
    1.10  end
    1.11  
    1.12 @@ -42,6 +42,10 @@
    1.13  instance ..
    1.14  end
    1.15  
    1.16 +lemma number_of_float_Float [code inline, symmetric, code post]:
    1.17 +  "number_of k = Float (number_of k) 0"
    1.18 +  by (simp add: number_of_float_def number_of_is_id)
    1.19 +
    1.20  lemma real_of_float_simp[simp]: "real (Float a b) = real a * pow2 b"
    1.21    unfolding real_of_float_def using of_float.simps .
    1.22  
    1.23 @@ -50,7 +54,7 @@
    1.24  lemma real_of_float_ge0_exp: "0 \<le> e \<Longrightarrow> real (Float m e) = real m * (2^nat e)" by auto
    1.25  
    1.26  lemma Float_num[simp]: shows
    1.27 -   "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and 
    1.28 +   "real (Float 1 0) = 1" and "real (Float 1 1) = 2" and "real (Float 1 2) = 4" and
    1.29     "real (Float 1 -1) = 1/2" and "real (Float 1 -2) = 1/4" and "real (Float 1 -3) = 1/8" and
    1.30     "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
    1.31    by auto