Isabelle2018: new "op x" syntax; now is "(x)"

(result of "isabelle update_op -m <dir>")

Isabelle2018: new comment syntax

(result of "isabelle update_comments <dirs>")

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.

x64 crefine: prove several lemmas in Retype_C

To prove that retyping a TCB establishes the state relation for TCBs,
it is necessary to prove that the C FPU null state is always equal to
the Haskell FPU null state. This commit therefore includes some
machinery for maintaining the state relation for the FPU null state,
and repairs many proofs.

x64 crefine: Refine_C sorry free

x64 crefine: close Arch_finaliseInterrupt sorry

crefine x64: Refine_C sorried

x64 crefine: ADT_C sorried, Init_C added

x64 crefine: add Syscall_C to Refine_C for testing

x64: crefine: add CSpace_C to Refine_C for regression testing

x64: crefine: add TcbAcc_C to Refine_C for testing

x64 crefine: adjust Refine_C to also use PSpace_C for testing

x64: change Refine_C to point to TcbQueue_C for regression testing

x64: add crefine stubs to keep theory_imports happy