On 22/04/17 11:48, Jasmin Blanchette wrote:
> I get the error
>
> Bad theory import "Main"
>
> Steps to reproduce the problem:
>
> cd src/HOL/Library
> isabelle jedit Cancellation.thy
Odd. I cannot reproduce this on Linux or macOS Sierra.
What is your $ISABELLE_HOME actually? Is there anything special with the
underlying file-system?
Here is an example for the Console/Scala toplevel within Isabelle/jEdit:
scala> PIDE.resources.session_base.known.files.toList.find(p =>
p._2.exists(_.theory == "Main"))
res0: Option[(java.io.File, List[isabelle.Document.Node.Name])] =
Some((/home/makarius/isabelle/repos/src/HOL/Main.thy,List(Main)))
What is your result?
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
