licenses: convert license tags to SPDX

asmrefine: update to Isabelle2019; reduce warnings

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.

Removes all trailing whitespaces

x64: create arch-specific CKernel

Isabelle2016-1: rename free variables to avoid capture

Isabelle2016-1: update references to renamed constants and facts

Handling of AsmStmt in c-parser, more tests.

The C-parser contains a full parser for __asm__ syntax but
up until now hasn't done anything with it. Instead we export
some semantics. It's unspecified exactly what these semantics
are but they are parametrised with the __asm__ semantics that
went in to them, so the translation validation has something
to reason about.

Tweak modifies proofs as a result, and add some more test files.

word_lib: adjust theory dependencies

Isabelle2016: SimplExportAndRefine updated for RC3

remove some cpat

gets CKernel to build

WIP on WCET annotations.

2015 update for CBaseRefine

fewer warnings

Fix to GlobalsSwap.thy in light of cc996ca9caa

Don't reuse the s_footprint_intvl theorem name.

Restore global valid assertions in graph refine.

The global-object pointer validity assertion is now created at
export time, and the graph refine mechanism now proves them. It
seems they were forgotten about once again in adjusting the globals
logic.

Fix asmrefine stuff for 2014 branch.

cspec: Updates for Isabelle 2014.

release cleanup

Import release snapshot.