[isabelle-dev] AFP/HLDE

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Oct 10 20:51:41 CEST 2018

> Can 'export_code' do that, with a slight modification to produce formal
> exports via Export.export?

That what indeed be feasible.

Instead of "file", a keyword like "prefix" could be given to "export_code".

I will put this into my pipeline to implement, but it will take some
time until this will take shape, the code generator printing layers are
very technical.


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

More information about the isabelle-dev mailing list