[isabelle-dev] HOL vs. HOL-Complex
brianh at cs.pdx.edu
Wed Jul 2 17:54:38 CEST 2008
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.
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.
More information about the isabelle-dev