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

[Stefan Berghofer]

Tobias Nipkow wrote:
> 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.

Really? In the thread

  http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/

cited by Brian and Alex, Brendan was worried about the fact that one could
no longer declare arities for sets. In my reply to his mail, I pointed
out that arities for sets could usually be rephrased as arities for functions
and booleans. I also asked him to give a concrete example for an arity where
this was not possible, but I never got a reply, so I assume that this is not
so much of a problem.

Greetings,
Stefan