[isabelle-dev] HOL vs. HOL-Complex
lp15 at cam.ac.uk
Thu Jul 3 11:15:19 CEST 2008
I am happy with this. I just wanted to remind everybody that the
nonstandard system allows really simple, intuitive proofs.
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
> 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...
More information about the isabelle-dev