#
9ede92c1 |
|
15-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get MPlambdaTheory to build again.
|
#
bc294d17 |
|
02-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Extract a usable half-way point from nominal_datatype branch. This replaces the is_perm predicate with a type embodying that predicate. It doesn't include the subsequent work on allowing multiple 'atom' types.
|
#
ba932e5d |
|
05-Jun-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rework lambda-theory scripts to use new varying parameter recursion theorem. Also make work for myself by having some of the script files use 'tight' equality. Later files get switched back to loose (prec = 100) equality, because it was all getting to be too much work.
|
#
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!
|
#
176a481a |
|
26-Nov-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixes for these examples, and an updated MANIFEST/README in other-models. The other-models directory had become particularly stale. I obviously need to check that it works more often. (Main problem: change to behaviour of Q.INST.)
|
#
aed05f4e |
|
20-Jul-2008 |
Konrad Slind <konrad.slind@gmail.com> |
A whole mess of small changes intended at making simpsets prettyprint informatively in the interactive loop. Very possibly I haven't updated all the files in the examples directories.
|
#
7cf5c42f |
|
09-Jul-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Completely reorganise these files into some sensible directories. Also, add a file demonstrating that the McKinna-Pollack two-sorted raw syntax does indeed behave properly (links appropriately to beta over quotiented terms).
|