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

[Lars Hupel]

> What are the remaining uses of these? How much of this can be integrated
> into the formal Isabelle session? How much of it is actually obsolete?

Hard to tell from a distance, but here's what I gather from reading the
Makefiles:

– Formal_SSA appears to download some file, unpack it, and compile
generated code together with it.

– Lightweight_Java generates an Isabelle theory file with Ott.

– Buchi_Complementation compiles generated code with MLton.

– Sturm_Sequences produces some extra LaTeX documentation. The generated
PDF is even committed to the AFP.

>   * no generated files in the repository (these are not sources but
> results from sources)

What about generated theory files? This also affects the CakeML entry. I
could easily package Lem as a component, but how would "isabelle build"
call it?