#
cdfdf71f |
|
29-Apr-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get examples/ARM/arm6-verification to build given tight-equality
|
#
9652789f |
|
29-Mar-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Support for simplifying and evaluating enumerated type representation/abstraction maps. For example, given Datatype `enum = one | two`; the following now works > EVAL ``num2enum 1``; val it = |- num2enum 1 = two: thm > EVAL ``enum2num two``; val it = |- enum2num two = 1: thm > SIMP_CONV (srw_ss()) [] ``enum2num two``; val it = |- enum2num two = 1: thm > SIMP_CONV (srw_ss()) [] ``num2enum 1``; val it = |- num2enum 1 = two: thm This also works when building custom compsets using computeLib. add_datatype_info. NOTE: This change may break some proofs (some in example/ARM have been fixed).
|
#
050df6ef |
|
01-Aug-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
Don't emit definition bindings for enumerated constants. Fixes #78. This commit also * fixes uses of constructor definitions (the equations are still present under the "number2<ty>_thm" name) * provides a regression test * a bug fix claim in the release notes.
|
#
4933479b |
|
01-Oct-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Word slice "<>" has been replaced with "''".
|
#
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!
|
#
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.
|
#
b842b27e |
|
11-Jul-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
examples/elliptic/arm -> examples/ARM/v4 examples/arm6 -> examples/ARM/arm6-verification
|