#
7e254797 |
|
03-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix some machine-code theories for pat_assum rename
|
#
1403e157 |
|
16-Jun-2015 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add a theorem about fun2set.
|
#
d455bab5 |
|
18-Dec-2011 |
Magnus Myreen <magnus.myreen@gmail.com> |
Various minor changes.
|
#
845531b5 |
|
14-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove trailing whitespace in source files.
|
#
bdcaf18d |
|
28-Feb-2011 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor tweaks.
|
#
999d6941 |
|
20-Dec-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Many minor additions/changes.
|
#
00a8819e |
|
09-Apr-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Minor update.
|
#
88c33b81 |
|
26-Mar-2010 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A general update.
|
#
90a751a1 |
|
05-Oct-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Many minor updates.
|
#
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!
|
#
9030ae5a |
|
26-Jun-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A general update: 1. the decompiler is now slightly faster, due to new code abbreviations (terms smaller in internal proofs); 2. the definition of the machine-code Hoare triple was slightly altered to support instruction caches; 3. the x86 model now includes an instruction cache. Also, I give up on attempting to support MoscowML for examples/machine-code/lisp. Both the standard kernel and the experimental kernel crash while loading files in this directory using the latest patched version of MoscowML. Both kernels exit with an uninformative message: Compiling lisp_equalScript.sml Linking lisp_equalScript.uo to produce theory-builder executable Uncaught exception: Chr Failed to build script file, lisp_equalScript Did they run out of memory? If so, why does the error message not say so?
|
#
44a6db21 |
|
03-Apr-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
Restructuring and simplification.
|
#
7c197d42 |
|
07-Jan-2009 |
Magnus Myreen <Magnus.Myreen@cl.cam.ac.uk> |
A new version of files previously in examples/mc-logic. Eventually examples/mc-logic will be deleted.
|