| #
91abdb57 |
|
08-Sep-2020 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
lib: add upcast_less_unat_less
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
|
| #
58866c62 |
|
04-Jun-2020 |
Rafal Kolanski <rafal.kolanski@data61.csiro.au> |
Word_Lib: add mask/le/unat lemmas from RISCV64 theories
neq_0_unat
unat_and_mask_le
sign_extend_less_mask_idem
word_and_le
le_smaller_mask
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
|
| #
62c8c799 |
|
26-Mar-2020 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
asmrefine: add missing signed cast rewrite
Signed-off-by: Edward Pierzchalski <ed.pierzchalski@data61.csiro.au>
|
| #
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
| #
1970ed0c |
|
21-Oct-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
word_lib internal + crefine: remove duplicate lemma
|
| #
9a1231bf |
|
20-Oct-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
word_lib internal: move up lemmas from Word_Lemmas_Internal
(non-AFP part)
|
| #
13143d72 |
|
21-Oct-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
word_lib internal: cleanup
|
| #
d2584a36 |
|
03-Sep-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
cleanup: collect word lemmas
|
| #
f3d95dbb |
|
04-Apr-2019 |
Rafal Kolanski <rafal.kolanski@data61.csiro.au> |
Word_Lib: add masking lemmas from RISCV64 lookup proofs
|
| #
65cc19c1 |
|
15-Mar-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: move up library lemmas from RISCV64 and X64
|
| #
21f9a86d |
|
19-May-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: sync Word_Lib with AFP
|
| #
d3713d79 |
|
16-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
lib: add some pure word lemmas found in proof/*
Preparation for removing duplicate word lemmas. These new lemmas
don't belong in the AFP word library, so we hook in to
`Word_Lemmas_Prefix` to expose them to our own theories.
|