src/HOL/Real/Hyperreal/Filter.ML
1998-12-11 paulson 1998-12-11 new Close_locale synatx
1998-11-27 paulson 1998-11-27 Addition of Hyperreal theories Zorn and Filter