The session HOL-NSA contains interesting material that deserves better visibility. How about renaming it to HOL-Nonstandard_Analysis, in analogy to HOL-Multivariate_Analysis? Makarius