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

Andreas Schropp schropp at in.tum.de
Fri Aug 26 18:20:21 CEST 2011

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

More information about the isabelle-dev mailing list