On 04/02/2019 08:00, Salomon Sickert wrote:
>
>
> To add a couple more to the list:
>
> — LTL has includes a parser that is used in an example and built using
> LTL/examples/build_poly.sh
>
> — LTL_to_DRA can generate a tool using either LTL_to_DRA/Code/build_poly.sh
> and LTL_to_DRA/Code/build_mlton.sh
It should be easy to make this part of the formal session, with some
options [condition = ISABELLE_MLTON].
The 'export_code' command will have to emit generated files
(Generated_Files.add_files) to make the assembly work in Isabelle/ML.
I have already added support for executable exports in
Isabelle/c175499a7537 -- a few more such fine-tunings might be required.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
