| #
9b2836ef |
|
19-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
word_lib: sync from AFP
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
|
| #
a424d55e |
|
09-Mar-2020 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
licenses: convert license tags to SPDX
|
| #
0fc9ab94 |
|
20-Oct-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
word_lib: add new material from l4v to AFP; cleanup
|
| #
e5ce178f |
|
20-Oct-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
word_lib: add mask_range
|
| #
21f9a86d |
|
19-May-2019 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
lib: sync Word_Lib with AFP
|
| #
b1aa74d3 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018 lib: Word_Lib
|
| #
19d9085b |
|
14-Jun-2018 |
Michael Sproul <michael.sproul@data61.csiro.au> |
lib: word lemma about mask and shiftl
|
| #
1ec4a8b1 |
|
03-Apr-2018 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
lib: miscellaneous word lemmas
|
| #
d108e3ed |
|
20-Dec-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
lib: a more intuitive definition of sign_extend for words
Also includes some supporting lemmas useful in bitfield proofs.
|
| #
edb30fa7 |
|
20-Dec-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
lib: faster simplification for common cases of word_and_max_word
In particular, this speeds up some bitfield proofs.
|
| #
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
| #
17586662 |
|
21-Feb-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
lib: add definition for word_ctz (count trailing zeros)
Nothing proved about this so far. Stated as most obvious formulation.
Needed for CParser to take in spec of __builtin_ctzl wrapper.
|
| #
e2ae586a |
|
13-May-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
word_lib: AFP document setup
|
| #
322f1023 |
|
18-Apr-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
word_lib: adjust theory dependencies
|
| #
445efb7c |
|
18-Apr-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
lib: closure for Word_Lib and own session
|
| #
1359602f |
|
17-Apr-2016 |
Gerwin Klein <gerwin.klein@nicta.com.au> |
word_lib: AFP naming conventions
|