| #
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>
|
| #
a7ed68e7 |
|
08-Apr-2020 |
Victor Phan <Victor.Phan@data61.csiro.au> |
x64 crefine/lib: move word lemmas out of Move_C into Word_Lemmas_64_Internal
Signed-off-by: Victor Phan <Victor.Phan@data61.csiro.au>
|
| #
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
| #
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.
|