somebody elses problem fixed
authornipkow
Thu Jun 07 11:25:27 2007 +0200 (2007-06-07)
changeset 232919179346e1208
parent 23290 c358025ad8db
child 23292 1c39f1bd1f53
somebody elses problem fixed
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/RealPow.thy	Thu Jun 07 11:25:05 2007 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Thu Jun 07 11:25:27 2007 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  done
     1.5  
     1.6  lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
     1.7 -by (simp add: real_le_square)
     1.8 +by (simp)
     1.9  
    1.10  lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
    1.11  by (simp add: abs_mult)