src/HOL/Library/Infinite_Set.thy

 
 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
   by (simp add: eventually_frequently)
 
 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
-  by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
+  by (simp add: cofinite_eq_sequentially)
 
 lemma
   shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
     and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   by (simp_all add: MOST_Suc_iff)

   shows "A = {}"
 using \<open>finite A\<close> A
 proof (induction A)
   case (insert a A)
   with R show ?case
-    by (metis empty_iff insert_iff) 
+    by (metis empty_iff insert_iff)
 qed simp
 
 corollary Union_maximal_sets:
   assumes "finite \<F>"
     shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>"