[isabelle-dev] HOL vs. HOL-Complex
makarius at sketis.net
Wed Jul 2 18:06:16 CEST 2008
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?
More information about the isabelle-dev