diff -r e0b46cd72414 -r 04d01ad97267 src/HOL/ex/HarmonicSeries.thy
--- a/src/HOL/ex/HarmonicSeries.thy	Tue Feb 23 10:37:25 2010 -0800
+++ b/src/HOL/ex/HarmonicSeries.thy	Tue Feb 23 11:14:09 2010 -0800
@@ -73,7 +73,8 @@
       qed
       moreover from xs have "x \<le> 2^m" by auto
       ultimately have
-        "inverse (real x) \<ge> inverse (real ((2::nat)^m))" by simp
+        "inverse (real x) \<ge> inverse (real ((2::nat)^m))"
+        by (simp del: real_of_nat_power)
       moreover
       from xgt0 have "real x \<noteq> 0" by simp
       then have
@@ -107,7 +108,7 @@
         by (auto simp: tmdef dest: two_pow_sub)
       also have
         "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^m"
-        by (simp add: tmdef realpow_real_of_nat [symmetric])
+        by (simp add: tmdef)
       also from mgt0 have
         "\<dots> = (real (2::nat))^(m - 1) / (real (2::nat))^((m - 1) + 1)"
         by auto
@@ -319,4 +320,4 @@
   ultimately show False by simp
 qed
 
-end
\ No newline at end of file
+end