On 26/09/2019 15:31, Makarius wrote:
>> 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".
>
> The theory name is actually "Concurrent_Revisions.OperationalSemantics"
BTW, you can also use completion on the theory base name, e.g. text
"Operational" followed by C+b in Isabelle/jEdit.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
