change definitions from SOME to THE

--- a/src/HOL/Hyperreal/HSeries.thy	Sun Sep 24 02:56:59 2006 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Sun Sep 24 03:38:36 2006 +0200
@@ -23,7 +23,7 @@
   "NSsummable f = (\<exists>s. f NSsums s)"
 
   NSsuminf   :: "(nat=>real) => real"
-  "NSsuminf f = (SOME s. f NSsums s)"
+  "NSsuminf f = (THE s. f NSsums s)"
 
 
 lemma sumhr:
@@ -179,8 +179,8 @@
 by (simp add: NSsums_def NSsummable_def, blast)
 
 lemma NSsummable_NSsums: "NSsummable f ==> f NSsums (NSsuminf f)"
-apply (simp add: NSsummable_def NSsuminf_def)
-apply (blast intro: someI2)
+apply (simp add: NSsummable_def NSsuminf_def NSsums_def)
+apply (blast intro: theI NSLIMSEQ_unique)
 done
 
 lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"

--- a/src/HOL/Hyperreal/Series.thy	Sun Sep 24 02:56:59 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Sun Sep 24 03:38:36 2006 +0200
@@ -24,7 +24,7 @@
    "summable f = (\<exists>s. f sums s)"
 
    suminf   :: "(nat=>real) => real"
-   "suminf f = (SOME s. f sums s)"
+   "suminf f = (THE s. f sums s)"
 
 syntax
   "_suminf" :: "idt => real => real"    ("\<Sum>_. _" [0, 10] 10)
@@ -97,15 +97,13 @@
 by (simp add: sums_def summable_def, blast)
 
 lemma summable_sums: "summable f ==> f sums (suminf f)"
-apply (simp add: summable_def suminf_def)
-apply (blast intro: someI2)
+apply (simp add: summable_def suminf_def sums_def)
+apply (blast intro: theI LIMSEQ_unique)
 done
 
 lemma summable_sumr_LIMSEQ_suminf: 
      "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
-apply (simp add: summable_def suminf_def sums_def)
-apply (blast intro: someI2)
-done
+by (rule summable_sums [unfolded sums_def])
 
 (*-------------------
     sum is unique