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 to mention type classes. It comes up again and again
on the mailing list.
>> Sticking with something merely to
>> avoid change is not a strong argument. This time we know what we go back
>> to and the real benefits (and the few losses).
>
> Do we really know?
>
> 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 this question just now...
The only gain I remember when we made the switch was that in some places
I could include precidates in set-theoretic terms, eg "even -> even".
Before I had to write something like "{x. even x} -> {x. even x}". How
the proofs changed in those places I do not remember.
Tobias
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
