Got it. In which case I agree with the split. Tobias
Brian Huffman wrote: > 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 >
