src/HOL/Hyperreal/Filter.thy
2006-06-20 ballarin 2006-06-20 Restructured locales with predicates: import is now an interpretation. New method intro_locales.
2005-09-12 huffman 2005-09-12 added theorem attributes transfer_intro, transfer_unfold, transfer_refold; simplified some proofs; some rearranging
2005-09-06 huffman 2005-09-06 reimplement Filter.thy with locales
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-07-31 paulson 2004-07-31 conversion of Hyperreal/{Fact,Filter} to Isar scripts
2000-12-30 paulson 2000-12-30 separation of HOL-Hyperreal from HOL-Real