I am also in favor of the set type-constructor. The issue of
compatibility with other HOL provers could very probably be solved by
the transfer mechanism. If not immediately from the generic setup, the
surely from a tailored one dedicated to this issue, if enough people are
concerned.
Amine.
On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
The benefits of getting rid of set were smaller than expected but quite
a bit of pain was and is inflicted.
Do you know of any more pain, apart from what Florian already mentioned?
Sticking with something merely to
avoid change is not a strong
Am 12/08/2011 11:27, schrieb Alexander Krauss:
On 08/12/2011 07:51 AM, Tobias Nipkow wrote:
The benefits of getting rid of set were smaller than expected but quite
a bit of pain was and is inflicted.
Do you know of any more pain, apart from what Florian already mentioned?
I think he omitted
It's clear that for inductive definitions, relations are frequently more
natural than sets. But I wonder whether a less drastic solution could have been
found than abandoning sets altogether. (I'm trying to imagine some sort of
magic operator to ease the transition between sets with various
On 08/12/2011 01:01 PM, Lawrence Paulson wrote:
(I'm trying to imagine
some sort of magic operator to ease the transition between sets with
various forms of tupling and relations.)
These tools exist to some extent, as the attributes [to_set] and
[to_pred]. It is used a few times in the
Surely we want to maintain both inductive and inductive_set?
Tobias
Am 12/08/2011 13:01, schrieb Lawrence Paulson:
It's clear that for inductive definitions, relations are frequently more
natural than sets. But I wonder whether a less drastic solution could
have been found than abandoning
On 08/12/2011 02:16 PM, Tobias Nipkow wrote:
Surely we want to maintain both inductive and inductive_set?
This is what Florian's experiment does. It basically reverts the 2008
transition, but not the 2007 one.
Alex
___
isabelle-dev mailing list
On Fri, Aug 12, 2011 at 2:27 AM, Alexander Krauss kra...@in.tum.de wrote:
What are, actually, the losses when going back? This has not yet been
touched by this thread at all (except the compatibility/import issue
mentioned by Brian), and at least myself I wouldn't feel comfortable
answering
On Fri, 12 Aug 2011, Alexander Krauss wrote:
Instead of stating an opinion, let me recall the parts of the story so
far that I know, to avoid that history repeats itself. I am sure that
Stefan will add some interesting details, too. (He wrote to me that it
may take him a few days to comment
On Fri, Aug 12, 2011 at 4:07 PM, Makarius makar...@sketis.net wrote:
http://isabelle.in.tum.de/repos/isabelle/rev/13e297dc improves startup
time of the worker thread farm significantly, and I've got real times in the
range of 0.003s -- 0.005s on my old machine from 2 years ago with Proof
10 matches
Mail list logo
