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: add obind_eqI_full to OptionMonad

Sometimes after showing equality of the heads of the obind, we need this
result in proof of equality of the tails.

lib: general update lemmas for opt_map

lib: move up library lemmas from RISCV64 and X64

lib: OptionMonad: add more obind decomposition, oassert simps

lib: more library lemmas for OptionMonad

global: isabelle update_cartouches

Base ASpec + machine on OptionMonad_ND; fix proof fallout

lib: option (reader) monad syntax and gets_map operator

Isabelle2018: Lib update

lib: make some elimination rules safer

Elimination against the pattern "P v", where both "P" and "v" are free,
can loop, if the rule is marked as a safe elimination rule. In the rules
modified in this commit, variable "v" provides no real benefit, so we
replace the pattern with "P".

Removes all trailing whitespaces

Isabelle2016-1: update references to renamed constants and facts

Monap_WP: fewer warnings

lib/spec/proof/tools: fix word change fallout

lib: start disentangling spaghetti word dependencies