# HG changeset patch
# User nipkow
# Date 1181208327 -7200
# Node ID 9179346e1208008dd28623cdaed3f757032e9667
# Parent  c358025ad8db894d4f95568d00d72dca1748be46
somebody elses problem fixed

diff -r c358025ad8db -r 9179346e1208 src/HOL/Real/RealPow.thy
--- 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)