[isabelle-dev] HOL vs. HOL-Complex

[Lawrence Paulson]

I am happy with this. I just wanted to remind everybody that the  
nonstandard system allows really simple, intuitive proofs.
Larry

On 2 Jul 2008, at 17:45, Brian Huffman wrote:

> Here's how I see it: If all you want to do is *use* analysis (e.g.  
> maybe you just want to calculate derivatives) then you won't notice  
> any difference between NSA and standard analysis. The same theorems  
> have been proved in either version. I expect that the users who  
> benefit most from having the real number theories in HOL would  
> generally fall into this camp.
>
> On the other hand, if you want to *prove* things *in* analysis, then  
> the difference between standard and non-standard is immediately  
> apparent.
>
> I wouldn't consider NSA to be "buried" - until very recently, the  
> NSA theories were located in a logic image separate from the main  
> HOL image. If we split NSA as I have proposed, then it will be in a  
> logic image separate from HOL, just as it was before.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20080703/f363331e/attachment.html>