Sure. Or maybe HOL-GCHQ? :-) Larry > On 26 Feb 2016, at 12:30, Makarius <makarius at sketis.net> wrote: > > 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?