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>
licenses: convert license tags to SPDX
lib: add @{inline_tactic} and @{inline_method} ML antiquotations This resurrects a useful part of the removed TacticAPI theory, with a much more generic implementation.