src/HOL/Nonstandard_Analysis/Hyperreal.thy
2016-02-29 wenzelm clarified session;
less more (0) tip