licenses: convert license tags to SPDX

lib: update for Isabelle 2019

lib: fix up Levity JSON output

- Previously printed `~` for negative numbers, which is invalid
JSON. Now prints `-`.

- Previously the outpout would unconditionally trim
'underscore-number' suffixes. Now uses theory context to determine
if it's likely to be an index into a theory list or an existing
fact name.

- Changed JSON structure to avoid using dynamic names for keys, i.e.
from this:

{
"my_theory_name": {...}
}

to this:

{
"theory": "my_theory_name",
"content": {...}
}

This should make processing the output slightly nicer by matching
what other tools expect.

- Changed JSON structure to consolidate dependencies. Lemmas are no
longer special-cased.

lib: change where temp file for AutoLevity tracing is created

We need to create the temp file on the same file system as the output
file in order for atomic renaming to work properly.

lib: log exceptions from AutoLevity trace writer

lib: fail gracefully if AutoLevity can't install hooks in unpatched Isabelle

lib: write autolevity traces on session shutdown

This commit depends on patching Isabelle to add a session shutdown hook.

Removes all trailing whitespaces

added missing license headers

autolevity: allow proof tracing level to be set with AUTOLEVITY environment variable

AUTOLEVITY=1 -- trace lemma dependencies, proof start/end
AUTOLEVITY=2 -- as above, also trace all dependent theorems per apply statement

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.

autolevity: add support for per-apply lemma dependency tracking

Also remove at-end theory hook due to unfinished proofs causing issues. Autolevity must be run from a completed session (see lib/AutoLevity_Run).

Per-apply dependency tracking requires a small isabelle patch.

autolevity: initial commit with test run on AInvs