--- a/src/HOL/Library/Infinite_Set.thy Wed Dec 28 23:24:18 2016 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Wed Dec 28 23:42:35 2016 +0100
@@ -152,7 +152,7 @@
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)"
@@ -317,7 +317,7 @@
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: