Hi all,
I have updated the Isabelle and AFP development repositories and cannot figure
how to do something pretty basic. I have my own theory, let's call it "Foo", in
a private repository outside the AFP, and "Foo" imports
"Concurrent_Revisions.Operational_Semantics" (i.e. "Operational_Semantics.thy"
from the "Concurrent_Revisions" AFP entry). Back in August, when launching
Isabelle/JEdit I would write
isabelle jedit -d ~/afp/thys Foo.thy
and that worked. (I also have 'init_component "$USER_HOME/afp"' in
"~/.isabelle/etc/settings".) But now (Isabelle/ffbe7784cc85 and
AFP/66bfe59e1850) this has stopped working. I get a red squiggly line under the
import of "Concurrent_Revisions.Operational_Semantics" in "Foo".
I studied the "isabelle jedit" options, as documented in "jedit.pdf", but
couldn't figure out how to proceed. I'd be grateful for any hint.
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
