[isabelle-dev] NEWS: generated code as proper theory export

Lars Hupel 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 mailing list