> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
