[isabelle-dev] Bad theory import "Main"
j.c.blanchette at vu.nl
Mon Apr 24 15:21:48 CEST 2017
> 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