# HG changeset patch
# User wenzelm
# Date 1482964955 -3600
# Node ID 47c1e6b0886fc9cfe6e7698f8f870c402305c03e
# Parent e991a4fab0dcf095af1a208df3648df4eda89160
tuned;
diff -r e991a4fab0dc -r 47c1e6b0886f src/HOL/Library/Infinite_Set.thy
--- 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)) \ (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 \ 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: