[isabelle-dev] HOL/Library

[Florian Haftmann]

> 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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20121122/7b90dc64/attachment.sig>