trivial: autocorres: add gen_word_heaps option, which forces all word heaps to be generated.
autocorres: update "autocorres" command documentation.
GHC 7.8 update (bitSize -> finiteBitSize)
import Haskell version of XN patch
enable XN in abstract spec; update AInvs and Refine
re-establish InfoFlow; generalising ptable_xn

UserOp_IF had its own way of extracting the XN bit from page tables.
This is now unified with the existing functions in ADT_AI, which also
means that the proof for XN bit equality is basically the same as for
pt_rights and pt_lift.
CRefine for XN
autocorres: Add struct initialiser testcase.

Previously the C parser has emitted (invalid) code that AutoCorres could
not handle. This testcase ensures that we can handle this case now.
lib: Add "solves" tactic.

Essentially does a "find_theorems solves" and automatically applies the
result.

The author makes no guarantees about the maintainability of proofs using
such a tactic.
Renamed "focus" to "subgoal". Used correct keyword tag (prf_goal) to fix batch processing.
autocorres: record which rules were used by L2Opt; enable using "trace_opt" option.

The traces are stored in AutoCorresData under the keys "{L2,HL,WA} {peephole,flow} opt".

"Trace" is currently a misnomer because we actually use Apply_Trace to
dig out the used facts afterward. Completeness is not guaranteed.
trivial: autocorres: documentation for trace_opt.