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: implement instantiate_thm for Trace_Schematic_Insts

This is a function that instantiates a thm with the instantiations provided by
trace_schematic_insts.

lib: restructure the instantiations type of Trace_Schematic_Insts

This allows us to explicitly record the bound variables from the subgoal so that
they can be more easily handled. We also now drop binders when constructing typ
instantiations.

lib: extend schematic instantiation tracer

Adds a combinator, `trace_schematic_insts_tac`, which wraps a rule-using
tactic and reports any schematic instantiations.

lib: trivial: use cartouches for ML comments.

Useful for antiquotations.

lib/Trace_Schematic_Insts: refactor; improve ML style

lib/Trace_Schematic_Insts: refactor and add code comments

lib/Trace_Schematic_Insts: some cleanup; add basic tests

lib: add trace_schematic_insts method combinator