somebody elses problem fixed

--- a/src/HOL/Real/RealPow.thy	Thu Jun 07 11:25:05 2007 +0200
+++ b/src/HOL/Real/RealPow.thy	Thu Jun 07 11:25:27 2007 +0200
@@ -41,7 +41,7 @@
 done
 
 lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
-by (simp add: real_le_square)
+by (simp)
 
 lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
 by (simp add: abs_mult)