| changeset 21854 | 42e9fd3ec1a3 |
| parent 21849 | a2e7a79159e4 |
| child 23280 | 4e61c67a87e3 |
--- a/src/HOL/Hyperreal/Filter.thy Thu Dec 14 21:46:59 2006 +0100 +++ b/src/HOL/Hyperreal/Filter.thy Thu Dec 14 22:08:35 2006 +0100 @@ -71,7 +71,7 @@ lemma (in freeultrafilter) singleton: "{x} \<notin> F" by (rule finite, simp) -lemma (in freeultrafilter) insert_iff: "(insert x A \<in> F) = (A \<in> F)" +lemma (in freeultrafilter) insert_iff [simp]: "(insert x A \<in> F) = (A \<in> F)" apply (subst insert_is_Un) apply (subst Un_iff) apply (simp add: singleton)