#
a45adef6 |
|
31-Oct-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
all: remove theory import path references In Isabelle2020, when isabelle jedit is started without a session context, e.g. `isabelle jedit -l ASpec`, theory imports with path references cause the isabelle process to hang. Since sessions now declare directories, Isabelle can find those files without path reference and we therefore remove all such path references from import statements. With this, `jedit` and `build` should work with and without explicit session context as before. Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
#
5deb58a9 |
|
23-May-2018 |
Thomas Sewell <Thomas.Sewell@data61.csiro.au> |
lib: add the Interference Trace Monad. Adds another style of monad to the existing ones in lib/Monad_WP. The Interference Trace monad is an extension of the nondeterministic state monad to record interactions between the task and its environment. It supports a parallel composition operator. The VCG for this monad includes the same Hoare triple style as for the state monads, and also includes a rely-guarantee quintuple which can be used to verify a parallel composition of programs.
|