[isabelle-dev] HOL vs. HOL-Complex

[Makarius]

On Wed, 2 Jul 2008, Brian Huffman wrote:

> The important point is that all the NSA stuff can be taken out without 
> losing any real functionality, since we are still left with a complete 
> development of *standard* analysis.

That's very interesting to hear.  Does it mean that there is no particular 
advantage in the NSA part anymore, unless you are specifically interested 
in the non-standard thing?


	Makarius