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.

Isabelle2018: Lib update

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

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

lib: fix AutoLevity JSON string encoding

Removes all trailing whitespaces

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: make output more JSON compliant

autolevity: make output JSON

autolevity: initial commit with test run on AInvs