On Wed, 2 Jul 2008, Brian Huffman wrote: > I wouldn't consider NSA to be "buried" - until very recently, the NSA > theories were located in a logic image separate from the main HOL image. > If we split NSA as I have proposed, then it will be in a logic image > separate from HOL, just as it was before.
The proposed HOL-NSA image could make nonstandard analysis even more visible --- not that I really mind either way. Makarius