| #
52062272 |
|
30-May-2017 |
Ramana Kumar <ramana@member.fsf.org> |
Fix ARM examples for length-nil
Part of #346
|
| #
c990a441 |
|
02-May-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix arm6-verification/correctness for new by
|
| #
119c7509 |
|
31-Jul-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix theories in arm6-verification/correctness
|
| #
354e6b14 |
|
21-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The overloading Tw is now temporary within wordsTheory.
|
| #
a6bf2df4 |
|
06-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Document Q.PAT_ABBREV_TAC. Also flip the default setting of "PAT_ABBREV_TAC: match var/const".
Warning: this change will break proofs that are sensitive to (rely on) the current behaviour of PAT_ABBREV_TAC.
See commits c5c281b, e824426, and a373506; and issue #79.
|
| #
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.
|
| #
f48c6820 |
|
16-Aug-2010 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fixes and tweaks following check-in 8434 (GENLIST moving to listTheory).
|
| #
a546c4a4 |
|
06-Dec-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Patch broken proofs.
|
| #
70a6204a |
|
29-Apr-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Repairs following changes to abbreviations.
|
| #
c2b09a35 |
|
01-Aug-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
The ARM6 example was failing to build (thanks to Hasan for spotting this).
The problem stems from changes made to the evaluated of w2w.
|
| #
b842b27e |
|
11-Jul-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
examples/elliptic/arm -> examples/ARM/v4
examples/arm6 -> examples/ARM/arm6-verification
|