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

[Andreas Schropp]

On 08/26/2011 06:33 PM, Brian Huffman wrote:
> This approach would let us avoid having to axiomatize the 'a set type.
>    

Thanks for trying to help me, but as I said:
   axiomatized set is just a slight inconvenience for me, so if you go for
sets as a seperate type don't bother introducing a new primitive.

> Also, for those of us who like predicates, "pred_typedef" might be
> rather useful as a user-level command.
>    

Sets and predicates are isomorphic, so if my isomorphic transfer tool works
out I don't see why this is needed.

> - Brian
>