[isabelle-dev] HOL vs. HOL-Complex

Tobias Nipkow nipkow at in.tum.de
Wed Jul 2 17:56:28 CEST 2008

Got it. In which case I agree with the split.


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

More information about the isabelle-dev mailing list