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

[Brian Huffman]

On Fri, Aug 26, 2011 at 1:23 PM, Andreas Schropp <schropp at in.tum.de> wrote:
> On 08/26/2011 10:38 PM, Makarius wrote:
>>
>> What is gained from that apart from having two versions of typedef?
>
> I am with you here.
> We don't need two primitive versions of typedefs.

This is incorrect: Only the predicate-based typedef need be primitive.
The set-based typedef can be implemented definitionally as a thin
layer on top of the predicate-based one.

- Brian