--- a/src/HOL/RealPow.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/RealPow.thy Wed Apr 29 14:20:26 2009 +0200
@@ -12,8 +12,6 @@
declare abs_mult_self [simp]
-instance real :: recpower ..
-
lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
by simp