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>

licenses: convert license tags to SPDX

lib: wp cleanup and parser improvements

The main visible change is from wp_trace', 'wp_once' and 'wp_once_trace' to
'wp (trace)', 'wp (once)' and 'wp (once, trace)'. The option for printing a
warning for unused supplied wp rules has also been removed.

global: isabelle update_cartouches

lib: update for Isabelle 2019

Isabelle2018: Lib update

Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

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.