equal
deleted
inserted
replaced
194 qed |
194 qed |
195 |
195 |
196 subsection {* Ultrafilter Theorem *} |
196 subsection {* Ultrafilter Theorem *} |
197 |
197 |
198 text "A locale makes proof of ultrafilter Theorem more modular" |
198 text "A locale makes proof of ultrafilter Theorem more modular" |
199 locale (open) UFT = |
199 locale UFT = |
200 fixes frechet :: "'a set set" |
200 fixes frechet :: "'a set set" |
201 and superfrechet :: "'a set set set" |
201 and superfrechet :: "'a set set set" |
202 |
202 |
203 assumes infinite_UNIV: "infinite (UNIV :: 'a set)" |
203 assumes infinite_UNIV: "infinite (UNIV :: 'a set)" |
204 |
204 |
400 by (rule freeultrafilter.intro [OF ultrafilter.intro]) |
400 by (rule freeultrafilter.intro [OF ultrafilter.intro]) |
401 (* FIXME: unfold_locales should use chained facts *) |
401 (* FIXME: unfold_locales should use chained facts *) |
402 qed |
402 qed |
403 qed |
403 qed |
404 |
404 |
405 lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex |
405 lemmas freeultrafilter_Ex = UFT.freeultrafilter_ex [OF UFT.intro] |
406 |
406 |
407 hide (open) const filter |
407 hide (open) const filter |
408 |
408 |
409 end |
409 end |