src/HOL/SEQ.thy
changeset 30082 43c5b7bfc791
parent 29803 c56a5571f60a
child 30196 6ffaa79c352c
     1.1 --- a/src/HOL/SEQ.thy	Tue Feb 24 11:10:05 2009 -0800
     1.2 +++ b/src/HOL/SEQ.thy	Tue Feb 24 11:12:58 2009 -0800
     1.3 @@ -338,10 +338,10 @@
     1.4  done
     1.5  
     1.6  lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
     1.7 -by (drule_tac k="1" in LIMSEQ_ignore_initial_segment, simp)
     1.8 +by (drule_tac k="Suc 0" in LIMSEQ_ignore_initial_segment, simp)
     1.9  
    1.10  lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
    1.11 -by (rule_tac k="1" in LIMSEQ_offset, simp)
    1.12 +by (rule_tac k="Suc 0" in LIMSEQ_offset, simp)
    1.13  
    1.14  lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
    1.15  by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)