camkes: Move libsel4 proofs to internal.
lib: misc lemmas.
lib: Helper for message register offsets.
lib: Generalise fst_enumerate, snd_enumerate; add some more helpers.
Check that install_C_file is given filename without bad characters

For the moment, it seems simplest just to check for the empty string and
for qualified IDs, both of which cause Isabelle pain.

JIRA VER-427
Implement C11's _Noreturn keyword.

JIRA VER-426
nicta-tools: Add "solved" tactic.

Ensures that all subgoals have been solved. If not, the tactic will fail
(causing backtracking).

Useful for creating proofs of the form:

    apply ((make_lots_of_subgoals, auto, solved)[1])

where you can be sure that the current subgoal will either be entirely
discharged or left untouched.
lib: Prove we can chop a word in half and put it back together.
lib: Generalise word_div_mult to operate on all words.
lib: Add collection of misc word helpers.
lib: Add a function for talking about word popcounts.
lib: more word helper lemmas.
lib: Rephrase popcount into def with to_bl.
Fix for JIRA VER-429 (with test-case)

The null-pointer value was not being given the right type when a
comparison was made with the zero literal.
memusage: Avoid race when fetching children of exiting process.
misc: Optimise filemerge scripts.

When streaming a large theory through these scripts, doing string replacements
line-by-line and repeated dictionary lookups become a significant performance
overhead. Relevant observable functionality should be unaffected by this
change.
infoflow: fixed and added Example_Valid_StateH to testing

Some of the noninterference results depend on executions at the haskell level starting at a valid initial state. This file demonstrates this condition being realised.
lib: Helper lemmas for simplifying writes via char pointers.
Merge branch 'master' of ssh://github.inside.nicta.com.au/seL4/l4v

Conflicts:
	lib/WordLemmaBucket.thy
lib: Random word lemmas about shift-left / shift-right / divide-by-zero.

Existing lemmas are (all?) conditional on the word size. These lemmas
are unconditional, albeit only work in the special case of "x >> 1" and
"x << 1".