# HG changeset patch
# User huffman
# Date 1315264060 25200
# Node ID 8478eab380e9af177cb4ccaf2a60d27bc5c2b49e
# Parent  d3bf0e33c98a60f79d20654d8b1d355c9a7c240c
generalize some lemmas

diff -r d3bf0e33c98a -r 8478eab380e9 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Sep 05 12:19:04 2011 -0700
+++ b/src/HOL/Series.thy	Mon Sep 05 16:07:40 2011 -0700
@@ -435,7 +435,7 @@
 by (simp add: summable_def sums_def convergent_def)
 
 lemma summable_LIMSEQ_zero:
-  fixes f :: "nat \<Rightarrow> 'a::real_normed_field"
+  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "summable f \<Longrightarrow> f ----> 0"
 apply (drule summable_convergent_sumr_iff [THEN iffD1])
 apply (drule convergent_Cauchy)
diff -r d3bf0e33c98a -r 8478eab380e9 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Sep 05 12:19:04 2011 -0700
+++ b/src/HOL/Transcendental.thy	Mon Sep 05 16:07:40 2011 -0700
@@ -54,7 +54,7 @@
 x}, then it sums absolutely for @{term z} with @{term "\<bar>z\<bar> < \<bar>x\<bar>"}.*}
 
 lemma powser_insidea:
-  fixes x z :: "'a::{real_normed_field,banach}"
+  fixes x z :: "'a::real_normed_field"
   assumes 1: "summable (\<lambda>n. f n * x ^ n)"
   assumes 2: "norm z < norm x"
   shows "summable (\<lambda>n. norm (f n * z ^ n))"
@@ -65,7 +65,7 @@
   hence "convergent (\<lambda>n. f n * x ^ n)"
     by (rule convergentI)
   hence "Cauchy (\<lambda>n. f n * x ^ n)"
-    by (simp add: Cauchy_convergent_iff)
+    by (rule convergent_Cauchy)
   hence "Bseq (\<lambda>n. f n * x ^ n)"
     by (rule Cauchy_Bseq)
   then obtain K where 3: "0 < K" and 4: "\<forall>n. norm (f n * x ^ n) \<le> K"