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

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

aspec: reintroduce spec document version information

Including version information in the spec document is tricky, because
Isabelle will rebuild the session whenever it sees that session inputs
(including document sources) have changed. Since ASpec is close to the
root of our session hierarchy, frequently changing version information
causes excessive rebuilds during development.

This commit avoids excessive rebuilding by building the document (with
version information) in a separate ASpecDoc session. The ASpecDoc
session is identical to the previous version of the ASpec session, but
is not the parent of any other sessions. The ASpec session is used as
the basis for other sessions, but has document-only inputs removed, and
also has document builds disabled.

licenses: update ignored cspec files for new kernel build system

x64: create arch-specific CKernel

arm-hyp: add missing license header

ignore C parser test files in license check

licenses: update ignored locations for moved cspec

haskell: use stack to obtain suitable GHC and cabal

trivial: ignore generated files in license check

backport changes to ARM proofs from X64 work in progress

- replace ARM-specific constants and types with aliases which can be
instantiated separately for each architecture.
- expand lib with lemmas used in X64 proofs.
- simplify some proofs.

Also-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>

update .licenseignore

trivial: skip jEdit .*.marks files in license check

When you right-click in the gutter to create a mark in the document,
jEdit creates a .filename.marks file which was confusing the license
check.

SELFOUR-421: fix coding style

CParser multi_arch_refactor: build standalone parser in dir named after arch

Architecture names follow L4V_ARCH-style naming conventions ('ARM', 'FAKE64').
However, the standalone parser does not make use of the L4V_ARCH environment
variable.

The standalone-parser Makefile builds all architectures at once, producing
binaries at 'ARM/c-parser', 'FAKE64/c-parser', and similarly for the tokenizer.

There are also wrapper scripts 'c-parser' and 'tokenizer' in the
standalone-parser directory, which take an architecture on the command line.

The make_munge.sh script calls the appropriate binary parser directly.

CParser multi_arch_refactor: fix tokenizer build

license-tool: .licenseignore update [VER-551]

license-tool: .licenseignore update + some fixes [VER-551]

license-tool: missing license headers + .licenseignore [VER-551]