camkes: ROOT updates

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>

camkes: remove NICTA logo

The logo can't be provided under an OSS license.

licenses: convert license tags to SPDX

CamkesCdlRefine: delete Generator theory

This theory was a project to specify the behaviour of the CAmkES
toolchain as an Isabelle function. However, this copy of the theory
is incomplete, the toolchain has moved on, and the ADL model is also
undergoing changes, so there is no longer much value in maintaining
this file.

camkes: support generalised connector semantics

The classic ADL formal model has a fixed palette of connectors, with
the interface type and seL4 integrity model also being fixed for each
connector type. This is unable to model new CAmkES connectors.

We change the ADL model to allow more combinations of connector
semantics, including arbitrary sets of Access rights between the
policy labels that a connector touches.

See Jira VER-1110 for more context.

CamkesCdlRefine: add support library for capDL refinement toolchain

This adds a library theory of useful lemmas, simpsets and methods,
to be used in the camkes-tool's capDL refinement templates.

camkes: remove ConnectorProperties_CAMKES theory

This was created long ago for a report and is no longer relevant.

camkes: initial updates for new CDL refinement framework

Summary of changes:
- change ADL spec to support connectors with many endpoints [VER-992]
- more connector synonyms
- refactor integrity policy spec

Isabelle2018 camkes: declare external file dependencies

Isabelle2018: add ulem.sty which is now required by isabelle.sty

(available by default in newer tetex installs, but not older ones)

Isabelle2018 spec: new handling of external file deps

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.

word_lib: adjust theory dependencies

camkes: Also depend on DPolicy in CamkesCdlBase.

camkes: Add WordLemmaBucket to the CamkesCdlBase session.

It occasionally comes in handy.

camkes: Add CAmkES↔CapDL beginnings.

These theories construct a locale with holes that are filled in by generated
code. Interpreting the locale manually is quite tedious and error prone, but we
entirely automate this process during code generation. For the details of this,
see the CAmkES 'architecture-semantics' and 'label-mapping' back ends.

camkes: Add CamkesCdlBase session.

This session encompasses the theories relevant for reasoning about the
relationship between CAmkES and CapDL.

camkes: Update ROOT files to Isabelle 2014.

Import release snapshot.