src/HOL/Hyperreal/Series.thy
changeset 20688 690d866a165d
parent 20552 2c31dd358c21
child 20689 4950e45442b8
     1.1 --- a/src/HOL/Hyperreal/Series.thy	Sun Sep 24 02:56:59 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/Series.thy	Sun Sep 24 03:38:36 2006 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4     "summable f = (\<exists>s. f sums s)"
     1.5  
     1.6     suminf   :: "(nat=>real) => real"
     1.7 -   "suminf f = (SOME s. f sums s)"
     1.8 +   "suminf f = (THE s. f sums s)"
     1.9  
    1.10  syntax
    1.11    "_suminf" :: "idt => real => real"    ("\<Sum>_. _" [0, 10] 10)
    1.12 @@ -97,15 +97,13 @@
    1.13  by (simp add: sums_def summable_def, blast)
    1.14  
    1.15  lemma summable_sums: "summable f ==> f sums (suminf f)"
    1.16 -apply (simp add: summable_def suminf_def)
    1.17 -apply (blast intro: someI2)
    1.18 +apply (simp add: summable_def suminf_def sums_def)
    1.19 +apply (blast intro: theI LIMSEQ_unique)
    1.20  done
    1.21  
    1.22  lemma summable_sumr_LIMSEQ_suminf: 
    1.23       "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
    1.24 -apply (simp add: summable_def suminf_def sums_def)
    1.25 -apply (blast intro: someI2)
    1.26 -done
    1.27 +by (rule summable_sums [unfolded sums_def])
    1.28  
    1.29  (*-------------------
    1.30      sum is unique