sys-init: Label all limitations of the system initialiser with "LIMITATION".
autocorres: experimental support for tracing heap_lift and word_abstract.

See tests/examples/TraceDemo.thy for an example.
noninterference: remove duplicate lemmas

Some redundant duplicate lemmas with duplicate names were proven under locale contexts 'unwinding_system' and 'complete_unwinding_system'.
lib: Add various word helper lemmas for bitfield proofs.
camkes: Move libsel4-related proofs to internal.
lib: Another bitfield helper lemma.
NICTACompat: Disable "Trace_Attrib".

Loading "Trace_Attrib" causes strange, unexplained lock-ups in
Isabelle/jEdit (and possibly Isabelle build). In particular, at random
times shortly after Trace_Attrib is loaded, everything will stop
processing with the CPU at 0%.

The root cause of this is currently unknown. This patch disables it
until the problem can be tracked down further.
Trace_Attribs: Remove hooks in "Corres_UL" to allow "lib/" to build once more.
misc: Add memory usage information to run_tests output.
trivial: run_tests: Tweak variable name.
trivial: run_tests: Reserve more visual space when printing memory usage.

The idea is that things should be right-aligned in the typical case.

99.99GB ought to be enough for anybody.
memusage: Ignore processes we don't have permission to stat.
memusage: Initally poll at a higher frequency to get better stats on short-lived processes.
ignore backup files
abstract Haskell init parameters into constants
lib: add some more bit manipulation helper lemmas.
lib: yet more helper lemmas.
lib: trivial helper for dealing with ∀ and pairs.

Comes in handy when juggling validNF_make_schematic_post in combination with a
Hoare triple with multiple bound variables.