--- 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