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

arch_split: fix proofs after removing shadow and unqualify commands and adding fix for crunch. Checks up to DPolicy.

arch_split: added namespacing to ExecSpec

l4v-sabre: minor fix on dmo_ackInterrupt and foldME

l4v-sabre: fix refine

WIP on handling array assertions. Up to Retype_C.

This is quite a lot of work in the end. I've had to gut most of
Retype_C along the way. Nearly done there.

fewer warnings

Import release snapshot.