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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Aug 25 23:26:55 CEST 2011

Hi Andreas,

> Let me ask something stupid:
>   why exactly do you guys axiomatize 'a set?
> Sure it's admissable and all, but why not do this definitionally
> via the obvious typedef?

the answer is rather technical: »typedef« in its current implementation
needs set syntax / set type as prerequisite.  Of course you could change
»typedef« to be based on predicates, but there is some kind of unspoken
agreement not to set one's hand on that ancient and time-honoured Gordon
HOL primitive.




PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110825/d9f50a7d/attachment.sig>

More information about the isabelle-dev mailing list