start Isabelle2014 udpate
Port AutoCorres to Isabelle 2014-RC0
Merge branch 'master' into isabelle-2014
add Lars' contribution
ported ASpec to Isabelle2014-RC0
some of the global Isabelle2014 renames

option_case -> case_option
sum_case -> case_sum
prod_case -> case_prod
Option.set -> set_option
Option.map -> map_option
option_rel -> rel_option
list_all2_def -> list_all2_iff
map.simps -> list.map
tl.simps -> list.sel(2-3)
the.simps -> option.sel
move isAligned to HaskellLib

Isabelle2014 doesn't like defs to be less general than the consts declaration.
CParser and lib tweaks; AutoCorres builds

CParser not finished yet, though: getting errors in cparser_test about linear
theory updates at end of thy.

Found more instances where we should be using Local_Theory.exit_global, but
might be besides the point (didn't help). Also might be overshooting the goal.
retire unused theories

Upto is broken by the removal of the finite_intvl_succ class
ported lib/* theories to Isabelle2014-RC0
option_map_def -> map_option_case for 2014-RC0
Proof updates, working as far as AInvs.
Refine working.
Fix Access, InfoFlow and DRefine.
More asmrefine work, global swapping ready.
ioapic: first abstract spec
Replace a clearly bad usage of Local_Theory.exit

See 8d2cfe7417cd for more in this vein.
Remove dodgy theory_of o Local_Theory.exit calls in hoare.ML
Comment out some parsing code and remove bad linear theory complaint.

This suggests there are bad things happening in the hoare package's
code for parsing (as the commented out code is simply a lemma
statement followed by oops).
Add a .gitignore for the tools/c-parser directory.