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

Stefan Berghofer berghofe at in.tum.de
Fri Aug 19 00:10:14 CEST 2011

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


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.


More information about the isabelle-dev mailing list