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: improve wp tracing

When tracing wp can now print the instantiated version of the rules being used.
It also says which set each used rule is from.

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

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.

lib: Datatype_Schematic and WPFix.

Add two new tactics/methods which can fix common painful problems with
schematic variables.

Method datatype_schem improves unification outcomes, by making judicious use of
selectors like fst/snd/the/hd to bring variables into scope, and also using a
wrapper to avoid singleton constants like True being captured needlessly by
unification.

Method wpfix uses strengthen machinery to instantiate rogue postcondition
schematics to True and to split precondition schematics that are shared across
different sites.

lib/wp: More aggressive version of wp_pre.

The previous wp_pre would apply a rule (from the named theorems wp_pre) unless
there was already a schematic in the goal. This is frequently prevented by an
irrelevant schematic.

This implementation applies a wp_pre rule unless one of the resulting goals
can be solved by "erule FalseE", that is, unless we would promote a schematic
into the assumption position (or, more rarely, there was already an assumption
schematic or False as an assumption).

wp: separate wp_pre method, used in wp and wpc