> 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?
Semantically, there is the issue of conflicting class instantiations,
which cannot be merged.
What has been added in more recent times is the tendency not to put
things into Library.thy which change the code generator setup on a
non-monotonic way. This rather technical requirement is the base for
Codegenerator_Test. This could be revisited as soon as ROOT files are
part of the interactive game.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
