#
c0633077 |
|
20-Aug-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix more missing ERR definitions
|
#
d35b02e2 |
|
28-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Restore ppstream_funs as nullary type operator in term_pp_types This name is used in user-written code (users' special purpose pretty-printers), and there is no reason to rebind this name, forcing them to change things.
|
#
21e53512 |
|
25-Mar-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get ARM examples to build; v7-step regression fails though
|
#
30f78bd2 |
|
14-Dec-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
User pp fns can note terms as binders to system printer This allows better behaviour in a test case shown to me by Mike, where annotations in monad-syntax weren't appearing.
|
#
994d4858 |
|
27-Aug-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Overhaul to rich_listTheory (it had become a bit of a disaster area). Some points: 1. rich_listTheory now uses the same constant names that are used in listTheory, e.g. TAKE instead of FIRSTN. 2. listTheory theorems are no longer replicated (saved again) in rich_listTheory. This avoids DB.match returning multiple instances of the same theorem. It also avoids saving around 100 theorems twice — in some cases after re-proving them. 3. Compatibility is now maintained though a bunch of SML "val" assignments added using adjoin_to_theory, e.g. val ZIP_FIRSTN_LEQ = ZIP_TAKE_LEQ val ALL_DISTINCT_SNOC = listTheory.ALL_DISTINCT_SNOC 4. Some incompatibilities are introduced: * FRONT___LENGTH is deleted, since it is the same as rich_listTheory.LENGTH_FRONT. * COUNT_LIST___ADD -> COUNT_LIST_ADD * COUNT_LIST___COUNT -> COUNT_LIST_COUNT * The compute theorems for COUNT_LIST and SPLITP have been renamed. * Some other theorems are no longer saved, e.g. rich_listTheory.list_INDUCT 5. Some theorems in listTheory have gained quantifiers.
|
#
88c9d19a |
|
06-Jan-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get ARM/v4's user-printer to compile again.
|
#
deb4dcca |
|
19-Nov-2009 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
adaption to the changes to userprinter
|
#
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!
|
#
8654de63 |
|
07-Feb-2009 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Attempt to tidy up (fix) EmitML and finish off the transition that Scott started. EmitML has been moved to the end of the build sequence. "Hooks" have been eliminated and all EmitML related stuff has been removed from the various theory directories. All code for generating ML/Caml is now self-contained within src/emit. I've not tested the generated Caml code but the SML seems to build fine. The directories: src/theoryML src/theoryOcaml src/emitScript have been replaced by src/emit/theories/ML src/emit/theories/Caml src/emit/theories
|
#
c67db89d |
|
25-Oct-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Fix required after changes to add_user_printer.
|
#
43ce388f |
|
19-Jun-2008 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Minor changes.
|
#
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.
|
#
415098a2 |
|
29-Apr-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
Misc. fixes to remove Mosml specific features.
|
#
b842b27e |
|
11-Jul-2007 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
examples/elliptic/arm -> examples/ARM/v4 examples/arm6 -> examples/ARM/arm6-verification
|