summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Extended_Real.thy

changeset 44890 | 22f665a2e91c |

parent 44669 | 8e6cdb9c00a7 |

child 44918 | 6a80fbc4e72c |

1.1 --- a/src/HOL/Library/Extended_Real.thy Sun Sep 11 22:56:05 2011 +0200 1.2 +++ b/src/HOL/Library/Extended_Real.thy Mon Sep 12 07:55:43 2011 +0200 1.3 @@ -1887,7 +1887,7 @@ 1.4 proof safe case goal1 1.5 have "ereal B < ereal (B + 1)" by auto 1.6 also have "... <= f n" using goal1 N by auto 1.7 - finally show ?case using B by fastsimp 1.8 + finally show ?case using B by fastforce 1.9 qed 1.10 qed 1.11 next 1.12 @@ -1916,7 +1916,7 @@ 1.13 proof safe case goal1 1.14 have "ereal (B - 1) >= f n" using goal1 N by auto 1.15 also have "... < ereal B" by auto 1.16 - finally show ?case using B by fastsimp 1.17 + finally show ?case using B by fastforce 1.18 qed 1.19 qed 1.20 next assume ?l show ?r