[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
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