On Thu, 19 Nov 2015, Lawrence Paulson wrote:
Library directory get special treatment. But I forget what this special
treatment consists of.
A long time ago, there was a slightly odd implicit load path for theories,
and src/HOL/Library was part of it by default. Thus it was possible to
import such theories without further decorations.
Nothing of that is relevant anymore.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
