generalize types of lim and nslim

--- a/src/HOL/Hyperreal/Lim.thy	Sun Sep 24 05:49:50 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Sun Sep 24 06:54:39 2006 +0200
@@ -1272,7 +1272,9 @@
 apply auto
 done
 
-lemma f_inc_imp_le_lim: "[| \<forall>n. f n \<le> f (Suc n);  convergent f |] ==> f n \<le> lim f"
+lemma f_inc_imp_le_lim:
+  fixes f :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>\<forall>n. f n \<le> f (Suc n); convergent f\<rbrakk> \<Longrightarrow> f n \<le> lim f"
 apply (rule linorder_not_less [THEN iffD1])
 apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc)
 apply (drule real_less_sum_gt_zero)
@@ -1291,7 +1293,9 @@
 apply (simp add: convergent_LIMSEQ_iff)
 done
 
-lemma g_dec_imp_lim_le: "[| \<forall>n. g(Suc n) \<le> g(n);  convergent g |] ==> lim g \<le> g n"
+lemma g_dec_imp_lim_le:
+  fixes g :: "nat \<Rightarrow> real"
+  shows "\<lbrakk>\<forall>n. g (Suc n) \<le> g(n); convergent g\<rbrakk> \<Longrightarrow> lim g \<le> g n"
 apply (subgoal_tac "- (g n) \<le> - (lim g) ")
 apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim)
 apply (auto simp add: lim_uminus convergent_minus_iff [symmetric])

--- a/src/HOL/Hyperreal/SEQ.thy	Sun Sep 24 05:49:50 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Sun Sep 24 06:54:39 2006 +0200
@@ -24,11 +24,11 @@
     --{*Nonstandard definition of convergence of sequence*}
   "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
 
-  lim :: "(nat => real) => real"
+  lim :: "(nat => 'a::real_normed_vector) => 'a"
     --{*Standard definition of limit using choice operator*}
   "lim X = (THE L. X ----> L)"
 
-  nslim :: "(nat => real) => real"
+  nslim :: "(nat => 'a::real_normed_vector) => 'a"
     --{*Nonstandard definition of limit using choice operator*}
   "nslim X = (THE L. X ----NS> L)"