lib: include ML_Goal_Test in ROOT

The file was not included anywhere so far and is referenced in ML_Goal,
which is part of the AutoCorres release (but the dependency
ML_Goal_Test will be missed if it's not included elsewhere).

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

lib: Isabelle2020 concurrency session

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

lib: Isabelle2020 update

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

ROOT files: file reorg for new ROOT requirements

Isabelle2020 requires each session to declare it own set of directories that
may not overlap with other session's directories. This commit reorganises
files to comply with that requirement.

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

licenses: convert license tags to SPDX

CamkesCdlRefine, Lib: add debug tag for integrity policy

This tags each generated policy goal with the object and cap that
led to that goal.

We create a new constant `generic_tag` in Lib for this purpose.

lib: move @{mk_term} antiquotation from AutoCorres; add examples

lib/RangeMap: cleanup; strengthen range lookup thms; add testsuite

lib: add RangeMap data structure (no tests yet)

lib: use `@{term_pat}` in FP_Eval; refactor term_pat testsuite

lib: initial version of FP_Eval tool

FP_Eval is an Isabelle/ML tool for functional program rewriting.
It has similarities with the Isabelle simplifier, but is simpler and
more scalable for performing computations in the logic.

See FP_Eval_Tests for basic tests and examples.

lib: Add tutorial on tactic basics.

This is an explicit walkthrough about how one goes about doing a proof
in Isabelle/ML. The goal is that someone can run into such a proof, look
at this tutorial, and then at least be equipped to ask the right
questions about fixing the proof.

lib: add ML utilties 'bucket' file.

The SML standard library is pretty bare-bones compared to that of other
functional languages, so in a large enough SML project you end up with a
bunch of reimplementations of basic combinators scattered all over the
place. We'd be able to collect them if we had somewhere to collect them,
so here it is.

lib: sep_tactics cleanup; session cleanup + organisation

lib: an abbreviation command with pretty printing inside locales

Normal abbreviations are not contracted on pretty printing when defined
inside a locale. This commit provide the command locale_abbrev which does
contract on pretty print even when defined inside a locale. It cannot be
used with abbreviations that mention fixed locale variables (whereas the
standard abbreviations can).

Co-authored-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>

lib: add FastMap tool

Many issues remain (see TODO list), but it's now mature enough to be
used for proof automation and has a comprehensive test suite.

lib: remove reference to removed theories in ROOT

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.

lib: move crunch tests to LibTest session

lib: test cases for Qualify tool

lib: test cases for Insulin and ShowTypes tools

lib: add Trace_Schematic_Insts_Test to LibTest

lib: move test theories in Lib to LibTest

Leaves out crunch tests, which seem fragile to being moved.

lib: add method to shorthand larger methods

Adds the `supply_local_method` command and `local_method` methods,
which store and apply methods as a way to shorten repeated
references to large or complicated methods.

lib/clib: move DetWPLib from CLib to Lib

Doesn't have any C dependencies.

lib: repair WPTutorial and CorresTest

Parts of CorresTest don't work any more after changes to the underlying
example functions.

lib: record AutoLevity session as broken

globally use session-qualified imports; add Lib session

Session-qualified imports will be required for Isabelle2018 and help clarify
the structure of sessions in the build tree.

This commit mainly adds a new set of sessions for lib/, including a Lib
session that includes most theories in lib/ and a few separate sessions for
parts that have dependencies beyond CParser or are separate AFP sessions.
The group "lib" collects all lib/ sessions.

As a consequence, other theories should use lib/ theories by session name,
not by path, which in turns means spec and proof sessions should also refer
to each other by session name, not path, to avoid duplicate theory errors in
theory merges later.