Most of the theories in there are loaded via Library.thy. But a few are loaded via ROOT. What is the rational for this subdivision? It looks like code generation is the difference, but why? Thanks Tobias