src/HOL/Filter.thy

 
 lemma le_sequentially:
   "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
   by (simp add: at_top_def le_INF_iff le_principal)
 
-lemma eventually_sequentiallyI:
+lemma eventually_sequentiallyI [intro?]:
   assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
   shows "eventually P sequentially"
 using assms by (auto simp: eventually_sequentially)
 
 lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"