Hi Makarius, > The problem is in the HOL-Lib session from isafor. It is somewhere in > your ROOTS (or -d specifications).
Ah! > Are you working with IsaFoR on purpose, or is this just an accident? That's it. I had IsaFoR as a component -- half on purpose, half by accident. Thanks for helping me debug it. > In current Isabelle/6acb28e5ba41 it is also possible to use something > like "isabelle jedit -R -l MY_SESSION" to restrict the theory name space > to the requirements of MY_SESSION. Good to know. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev