[isabelle-dev] HOL/Library

Tobias Nipkow nipkow at in.tum.de
Wed Nov 21 08:17:35 CET 2012


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


More information about the isabelle-dev mailing list