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 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...

I am not arguing against 'a set, but please bring the facts to light! That we have to discuss this now is mainly since the last switch was made without fully evaluating the consequences (even though they were known already at the time).

Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to