[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
krauss at in.tum.de
Fri Aug 12 11:27:32 CEST 2011
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).
More information about the isabelle-dev