History log of /seL4-l4v-master/l4v/lib/Word_Lib/Word_Lemmas_32_Internal.thy
Revision Date Author Comments
# 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>
# 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.