1.1 --- a/src/HOL/Library/Float.thy	Tue Apr 28 19:15:50 2009 +0200
     1.2 +++ b/src/HOL/Library/Float.thy	Wed Apr 29 14:20:26 2009 +0200
     1.3 @@ -443,8 +443,6 @@
     1.4  lemma Ifloat_min: "Ifloat (min x y) = min (Ifloat x) (Ifloat y)" unfolding min_def le_float_def by auto
     1.5  lemma Ifloat_max: "Ifloat (max a b) = max (Ifloat a) (Ifloat b)" unfolding max_def le_float_def by auto
     1.6  
     1.7 -instance float :: recpower ..
     1.8 -
     1.9  lemma float_power: "Ifloat (x ^ n) = Ifloat x ^ n"
    1.10    by (induct n) simp_all
    1.11