Remove pure word lemmas from proof/*

Removes redundant lemmas after moving them up to Word_Lib.

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>")

c-parser: qualified session imports; Word_Lib base image

Previously, everything was counted under session CParser, incl most of
Word_Lib. The dependency on Word_Lib thus revealed means Word_lib is the
better base image for session Simpl-VCG.

manually adjust non-obvious cases of tab to space replacement

remove most tab characters

x64: configure arch-specific array types

Isabelle2016-1: update references to renamed constants and facts

lib: fix theory includes for arch-splitted WordSetup

lib: fix theory includes for arch-splitted WordSetup

c-parser: factor out more 32-bit dependencies in umm_heap

If one changes the occurrences of 32 in Addr_Type to 64, everything up
to CTranslation still builds successfully.

Work towards JIRA VER-487

c-parser: add packed_type instance for 2D arrays

I finally got it down into a form that Isabelle accepts, and without
even having to add spurious axioms.

2015 update progress

Port AutoCorres to Isabelle 2014-RC0

Import release snapshot.