[isabelle-dev] Proposal for localized interpretations

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Nov 26 15:59:17 CET 2014

Hi Andreas, hi Jasmin,

> It's quite nice as it is. Thanks!
> Andreas: I think I promised to help you with the code generator and "code_datatype" (cf. our private email conversation about "Quickcheck & Codatatypes"). I don't understand "code_datatype" (or what you do with it) well enough to do it without guidance, but if you are still interested please relaunch me on that, ideally after December 7.

In my understanding, this seems quite trivial.  The first step is to
formally generalize the existing registration functions with
Plugin_Name.filter arguments (from data_default to data):



Then the input syntax is adjusted accordingly using
Pluing_Name.parse_filter, e.g.


Does this help?

All the best,


PGP available:

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

More information about the isabelle-dev mailing list