[isabelle-dev] NEWS: generated code as proper theory export
hupel at in.tum.de
Fri Feb 1 16:40:06 CET 2019
> The standard approach for the latter is to have the other tool directly
> import its source format into the theory context within Isabelle/ML,
> without the intermediate theory source. Doing this carefully, would even
> produce nice PIDE markup for the original sources. PIDE is an IDE for
> arbitrary user-defined languages.
> It might be worth doing this for tools like Lem eventually, but I have
> not looked at it closely so far.
Lem is implemented in OCaml, so this seems like a stretch. I'd say
importing HOL4 into Isabelle is a more plausible solution.
More information about the isabelle-dev