[isabelle-dev] typedef (open) legacy

[Florian Haftmann]

> I think either option 3 or 4 would make sense, although I'd say 4 is
> preferable for a couple of reasons: First, it makes the implementation
> of typedef simpler. Second, it actually gives users more flexibility
> because if they want a set constant, they can use any definition
> package, not just "definition". The extra verbosity in some cases is a
> small price to pay.

I would support (4).  In the long run, typedef should be the bare
foundational minimum for introducing HOL types, whereas all user-level
features could go to a command type_definition with support for the
quotient package, reasonable user-level rules, code generator setup etc.

	Florian

-- 

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: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121004/28b2cb8f/attachment.sig>