src/HOL/Real_Vector_Spaces.thy
changeset 59587 8ea7b22525cb
parent 58889 5b7a9633cfa8
child 59613 7103019278f0
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Mar 04 23:31:04 2015 +0100
     1.3 @@ -1521,9 +1521,8 @@
     1.4  lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
     1.5    unfolding filterlim_at_top
     1.6    apply (intro allI)
     1.7 -  apply (rule_tac c="natceiling (Z + 1)" in eventually_sequentiallyI)
     1.8 -  apply (auto simp: natceiling_le_eq)
     1.9 -  done
    1.10 +  apply (rule_tac c="nat(ceiling (Z + 1))" in eventually_sequentiallyI)
    1.11 +  by linarith
    1.12  
    1.13  subsubsection {* Limits of Sequences *}
    1.14