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

[Florian Haftmann]

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.

Rgds.,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>