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

[Lars Hupel]

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