[isabelle-dev] Bad theory import "Main"

Blanchette, J.C. j.c.blanchette at vu.nl
Mon Apr 24 15:21:48 CEST 2017

Hi Makarius,

> The problem is in the HOL-Lib session from isafor. It is somewhere in
> your ROOTS (or -d specifications).


> 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.


More information about the isabelle-dev mailing list