[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

[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?

> 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