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

[Andreas Schropp]

On 08/26/2011 10:50 PM, Brian Huffman wrote:
> 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.
>    

That is exactly what I said below the quoted line. ;>
I guess this discussion only came about because you said HOL4-style
typedefs, which cannot be used as the primitive.

> - Brian
>