summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/Infinite_Set.thy

changeset 64697 | 47c1e6b0886f |

parent 63993 | 9c0ff0c12116 |

child 64967 | 1ab49aa7f3c0 |

--- 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: