src/HOL/Real_Vector_Spaces.thy
changeset 61942 f02b26f7d39d
parent 61916 7950ae6d3266
child 61969 e01015e49041
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Sun Dec 27 17:16:21 2015 +0100
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sun Dec 27 21:46:36 2015 +0100
     1.3 @@ -1701,8 +1701,10 @@
     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="nat(ceiling (Z + 1))" in eventually_sequentiallyI)
     1.8 -  by linarith
     1.9 +  apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI)
    1.10 +  apply linarith
    1.11 +  done
    1.12 +
    1.13  
    1.14  subsubsection \<open>Limits of Sequences\<close>
    1.15