[isabelle-dev] HOL vs. HOL-Complex
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