[isabelle-dev] HOL vs. HOL-Complex

[Brian Huffman]

Quoting Tobias Nipkow <nipkow at in.tum.de>:

> I don't use Complex, but I strikes me as odd that some of our complex
> theories should be in the HOL image and other should not be. What is
> the rational for splitting something off? Only because it is based on
> NSA? Does a user care how something is defined?
>
> Just wondering.
>
> Tobias

It's not that some things are defined via NSA and others are not.  
Rather, HOL-Complex defines separate standard and nonstandard versions  
of just about every concept in analysis: Cauchy sequences,  
convergence, limits, continuity, derivatives, you name it. The NSA  
theories are essentially a parallel development of analysis; the  
standard theories do not depend on them at all. (At least, they don't  
any more - they used to, before I started hacking on HOL-Complex.)

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.

- Brian