changeset 60036 | 218fcc645d22 |
parent 59867 | 58043346ca64 |
child 60041 | 6c86d58ab0ca |
--- a/src/HOL/NSA/StarDef.thy Sun Apr 12 16:04:53 2015 +0200 +++ b/src/HOL/NSA/StarDef.thy Sun Apr 12 11:33:19 2015 +0200 @@ -5,7 +5,7 @@ section {* Construction of Star Types Using Ultrafilters *} theory StarDef -imports Filter +imports Free_Ultrafilter begin subsection {* A Free Ultrafilter over the Naturals *}