My $0,02: I was wondering about the merge as well. For my taste, there is
almost too much in HOL already as it is.
It's not such a big problem, though. You can always build your own custom
images with exactly the part you need (not that it's a nice user-interface
paradigm, and you need to
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
Url :
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080702/7157af62/attachment.pgp
Very nice job!
Amine.
PS: In Reflected Ferrack you start combutation with True, i.e. @{code
T}, if the input is @{term False}. Fortunately this does not happen
often Even with @{code} we still need to be careful...
Florian Haftmann wrote:
New ML antiquotation 'code': takes constant as
Quoting Florian Haftmann florian.haftmann at informatik.tu-muenchen.de:
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
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
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
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
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
Quoting Makarius makarius at sketis.net:
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 lp15 at cam.ac.uk:
I see a giant misconception coming. The point of nonstandard
