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