| changeset 28823 | dcbef866c9e2 |
| parent 27681 | 8cedebf55539 |
| child 36176 | 3fe7e97ccca8 |
--- a/src/HOL/NSA/Filter.thy Mon Nov 17 17:00:27 2008 +0100 +++ b/src/HOL/NSA/Filter.thy Mon Nov 17 17:00:55 2008 +0100 @@ -77,10 +77,9 @@ apply (simp add: singleton) done -lemma (in freeultrafilter) filter: "filter F" by unfold_locales +lemma (in freeultrafilter) filter: "filter F" .. -lemma (in freeultrafilter) ultrafilter: "ultrafilter F" - by unfold_locales +lemma (in freeultrafilter) ultrafilter: "ultrafilter F" .. subsection {* Collect properties *}