lib + proof: Isabelle2020 Method.NO_CONTEXT_TACTIC rename

Method.NO_CONTEXT_TACTIC -> NO_CONTEXT_TACTIC

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

lib: Isabelle2020 update

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

licenses: convert license tags to SPDX

global: isabelle update_cartouches

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

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

lib: adjust some congruence rules for strengthen.

Adjusting the strengthen congruence rules for conjunction
and disjunction makes other conjuncts available as assumptions
in strengthening a conjunction. This may be useful occasionally.

trivial lib: quote identifiers in text blocks for document builds

Demo theory for strengthen.

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.

Spring cleaning in strengthen.

Make the tactic steps more explicit, especially involving the -oblig-
premises for which I've seen a bug in the past.

Removes all trailing whitespaces

make strengthen method Eisbach-compatible

SELFOUR-444: Fix for rebase.

Fix a bug with strengthen rules.

Adding optional tracing makes the bug clear; the subgoals of the
rules are attacked in the opposite order, so congruence-style rules
which introduce extra assumptions would have the (schematic)
assumptions unified out of order. Fixed.

lib: start disentangling spaghetti word dependencies