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)
On Wed, 2 Jul 2008, Brian Huffman wrote:
> 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
On Wed, 2 Jul 2008, Brian Huffman wrote:
> 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.
That's very interesting to hear. Does it mean that there is no partic
Got it. In which case I agree with the split.
Tobias
Brian Huffman wrote:
> Quoting Tobias Nipkow :
>
>> 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
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
Brian Huffman
I see a giant misconception coming. The point of nonstandard analysis
is that it makes properties of limits, derivatives, and so forth much
easier to prove than can be done with the standard definitions. They
eliminate the necessity of arguments involving epsilon and delta. So
it would be a
Quoting Makarius :
> Does it mean that there is no particular
> advantage in the NSA part anymore, unless you are specifically interested
> in the non-standard thing?
Quoting Lawrence Paulson :
> I see a giant misconception coming. The point of nonstandard analysis
> is that it makes properties
Quoting Tobias Nipkow :
> 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
Quoting Florian Haftmann :
> There is no urgent need that the HOL image contains *all* the
> HOL-Complex theories. I also have been thinking about splitting off all
> the Analysis stuff into a session HOL-Analysis, but on the other hand a
> lot of functions which you naively expect for reals/comp
what I forgot to mention:
There is no urgent need that the HOL image contains *all* the
HOL-Complex theories. I also have been thinking about splitting off all
the Analysis stuff into a session HOL-Analysis, but on the other hand a
lot of functions which you naively expect for reals/complexes (lo
Hi Brian,
first of all, I want to emphasize that the merging of HOL-Complex with
HOL is not necessarily the final state. We are still experimenting and
collecting feedback,
> What is the rationale behind merging HOL-Complex with HOL?
> I would guess that the real reason for the merge is that som
11 matches
Mail list logo
