[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 25 23:26:55 CEST 2011
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev