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: various crunch improvements

The main one is that crunch now uses wpsimp when determining whether a goal
can already be solved, instead of just wp. Crunch can also now use wps
when proving a goal and will now always ignore a constant if told to, even
if it is the top-level constant being crunched.

global: isabelle update_cartouches

Isabelle2018: Lib update

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

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

Upgrade strengthen for assumptions, methods.

The strengthen implementation can now do a bit more.

The new method strengthen_asm also adjusts assumptions.

The new method strengthen_meth takes a method as a parameter,
e.g. apply (strengthen_meth \<open> rule order.trans \<close>)
does the same thing as apply (strengthen order.trans)
with scope for other exciting applications I haven't thought of.

Removes all trailing whitespaces

Isabelle2016-1: update references to renamed constants and facts

lib: start disentangling spaghetti word dependencies