--- a/src/HOL/Real_Vector_Spaces.thy Sun Dec 27 17:16:21 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Sun Dec 27 21:46:36 2015 +0100
@@ -1701,8 +1701,10 @@
lemma filterlim_real_sequentially: "LIM x sequentially. real x :> at_top"
unfolding filterlim_at_top
apply (intro allI)
- apply (rule_tac c="nat(ceiling (Z + 1))" in eventually_sequentiallyI)
- by linarith
+ apply (rule_tac c="nat \<lceil>Z + 1\<rceil>" in eventually_sequentiallyI)
+ apply linarith
+ done
+
subsubsection \<open>Limits of Sequences\<close>