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

Reply via email to