[isabelle-dev] HOL vs. HOL-Complex

Makarius makarius at sketis.net
Wed Jul 2 19:18:12 CEST 2008

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.


More information about the isabelle-dev mailing list