changeset 55018 | 2a526bd279ed |
parent 52198 | 849cf98e03c3 |
child 58878 | f962e42e324d |
--- a/src/HOL/NSA/Filter.thy Thu Jan 16 16:20:17 2014 +0100 +++ b/src/HOL/NSA/Filter.thy Thu Jan 16 16:33:19 2014 +0100 @@ -7,7 +7,7 @@ header {* Filters and Ultrafilters *} theory Filter -imports "~~/src/HOL/Library/Zorn" "~~/src/HOL/Library/Infinite_Set" +imports "~~/src/HOL/Library/Infinite_Set" begin subsection {* Definitions and basic properties *}