| #
d7574020 |
|
20-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Remove pure word lemmas from proof/*
Removes redundant lemmas after moving them up to Word_Lib.
|
| #
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)"
(result of "isabelle update_op -m <dir>")
|
| #
4fedfb5e |
|
06-May-2018 |
Michael Sproul <michael.sproul@data61.csiro.au> |
x64: crefine: clear remaining sorry in Interrupt_C (VER-879)
|
| #
bcac2c84 |
|
01-Feb-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
x64: clear some sorry proofs from CSpace_C
Also update some Haskell and abstract specs relating to IO ports.
|
| #
25abf2b9 |
|
07-Jan-2018 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: onle Arch_decodeIRQControlInvocation_ccorres remains in Interrupt_C
|
| #
ff95aec2 |
|
09-Nov-2017 |
Joel Beeren <joel.beeren@data61.csiro.au> |
x64: crefine: added Interrupt_C
|