[isabelle-dev] HOL vs. HOL-Complex

[Makarius]

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