summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | huffman |

Tue, 23 Feb 2010 11:14:09 -0800 | |

changeset 35345 | 04d01ad97267 |

parent 35344 | e0b46cd72414 |

child 35346 | 8e1f994c6e54 |

adapt to changes in simpset

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