| changeset 55018 | 2a526bd279ed |
| parent 52198 | 849cf98e03c3 |
| child 58878 | f962e42e324d |
| 55017:2df6ad1dbd66 | 55018:2a526bd279ed |
|---|---|
5 *) |
5 *) |
6 |
6 |
7 header {* Filters and Ultrafilters *} |
7 header {* Filters and Ultrafilters *} |
8 |
8 |
9 theory Filter |
9 theory Filter |
10 imports "~~/src/HOL/Library/Zorn" "~~/src/HOL/Library/Infinite_Set" |
10 imports "~~/src/HOL/Library/Infinite_Set" |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Definitions and basic properties *} |
13 subsection {* Definitions and basic properties *} |
14 |
14 |
15 subsubsection {* Filters *} |
15 subsubsection {* Filters *} |