diff -r 6df83a636e67 -r f763367e332f src/HOL/Hyperreal/Lim.thy
--- 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])