[isabelle-dev] Incoherent use of file name "hoare_syntax.ML"

Lars Hupel lars at hupel.info
Fri Jan 1 18:16:20 CET 2021

> The approach looks right: a theory context manages shared resources according
> to the import graph structure.

Sadly we now have a "total existence failure", as evidenced in


It appears that the JVM process just hangs when (or after) building the 
document for the Network_Security_Policy_Verification session.

(Logfiles and Session DBs are available for download: 

More information about the isabelle-dev mailing list