[isabelle-dev] AFP/HLDE

[Florian Haftmann]

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

Cheers,
	Florian

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