#
cba5259c |
|
15-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix ARM/v4 example for tight equality
|
#
3db8b2bb |
|
21-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The overloading Tw is now temporary within wordsTheory.
|
#
a2328149 |
|
23-Sep-2011 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
a47af14f |
|
14-Feb-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Repairs: replacing "$-"` with "-".
|
#
f8131891 |
|
20-Jan-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Test out using using unadorned underscores in case statements. Also added derived theorems for "ADD rd, pc, #n" and "SUB rd, pc, #n".
|
#
fc55b083 |
|
20-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor tweaks to improve the presentation of ARM_MSR and ARM_SBC theorems.
|
#
0100e400 |
|
01-May-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Renamed bsubst to update (as it is in v4T). Moved a few definitions/theorems to better homes.
|
#
d080e6cd |
|
19-Mar-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Have rationalised the treatment cases for words, changing word_nchotomy to ranged_word_nchotomy. This means that "Cases" and "Cases_on" now subsume "wordsLib.Cases_word" and "wordsLib.Cases_on_word". Have eliminated some occurrences of the latter.
|
#
e5c18972 |
|
24-Jan-2008 |
Peter Homeier <palantir@trustworthytools.com> |
Revised expressions of the form <term>:<type> ' <term> to be (<term>:<type>) ' <term> to avoid confusion with the type variable ' .
|
#
82dbf67d |
|
18-Jan-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fixed broken proofs - following addition of WORD_ss to srw_ss(). Also replaced %% with '.
|
#
d05e3e81 |
|
05-Dec-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Added PC relative STR and LDR.
|
#
87a1e200 |
|
06-Nov-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix parsing/printing for UMULL etc.
|
#
b842b27e |
|
11-Jul-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
examples/elliptic/arm -> examples/ARM/v4 examples/arm6 -> examples/ARM/arm6-verification
|