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

[Tobias Nipkow]

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