[isabelle-dev] HOL vs. HOL-Complex

[Tobias Nipkow]

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
>