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
