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 message printing for crunch and wp, and refactor common printing functions

global: isabelle update_cartouches

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

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

Isabelle2018 lib: Apply_Trace

Isabelle2017: update lib for RC0

* ML Proof_Context.fact_alias renamed to alias_fact.

* Named_Target.init removed redundant parameter.

* Simplified Greatest, removed GreatestM.

* Introduced thm_node type in proofterm.ML.

manually adjust non-obvious cases of tab to space replacement

remove most tab characters

Removes all trailing whitespaces

Fix bug in apply_trace when used with grouped lemmas.

This commit fixes a typo in apply_trace which
prevented correct printing of the index of
the lemma used in a grouped lemma.
An example is given in Apply_Trace_Cmd.thy

apply_trace: general interface for printing

apply_trace: attempt to give local facts

Do some name-mangling to try to find the most local variant of a fact

Isabelle2016-1: update to new ML API

Update references to renamed ML constants; supply default arguments to
functions with additional parameters; etc.

autolevity: refine tracing apply everywhere to work via Proof module hooks

This avoids doing redundant tactic operations at the top-level and lets
us trace "by" statements easily.

apply_trace: avoid conjunctionI before tracing

isabelle-2016: update Apply_Trace and fix to work in batch mode.

2016: attempt to update Apply_Trace.thy

fixed Apply_Trace (removed broken mentioned_facts feature)

fixed Apply_Trace (removed broken mentioned_facts feature)

start work on Isabelle 2015 update

Fixed apply trace for Isabelle 2014

apply_trace: Add lower-level interface for clearing/reading deps.

The lower-level interface is useful for ML hackers, trying to debug
their own ML tactics.

Port AutoCorres to Isabelle 2014-RC0

Import release snapshot.