src/HOL/Library/Float.thy

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