| #
76df2820 |
|
12-Sep-2010 |
Matt Kaufmann <kaufmann@cs.utexas.edu> |
Modified boilerplate for generated ML files, which now end in .sml instead of .ml and have underscores in filenames in place of hyphens.
|
| #
7ac37058 |
|
19-Aug-2010 |
Matt Kaufmann <kaufmann@cs.utexas.edu> |
Eliminated remaining include-book events from generated .ml files.
|
| #
ce087f2f |
|
19-Aug-2010 |
Matt Kaufmann <kaufmann@cs.utexas.edu> |
Added ISSUES file and implemented change leading to first issue: ACL2 include-book forms no longer generate ML.
|
| #
7b313d7a |
|
17-Aug-2010 |
Matt Kaufmann <kaufmann@cs.utexas.edu> |
More support for ACL2 packages, eliminating generation of defpkg forms in ML.
|
| #
0ca049cf |
|
17-Aug-2010 |
Matt Kaufmann <kaufmann@cs.utexas.edu> |
Fixed Lisp package issues.
|
| #
9defa685 |
|
17-Aug-2010 |
Matt Kaufmann <kaufmann@cs.utexas.edu> |
Updates to handle packages; also addition of jvm M1 model
|
| #
d18f5d4b |
|
08-Dec-2008 |
Matt Kaufmann <kaufmann@cs.utexas.edu> |
Updated to the latest version (3.4) of ACL2 and did some
reorganization and addition to support regression testing.
Pathnames only need to be edited in one place now:
.acl2holrc.bash
Edited and added README files. In particular, tests/README explains
how to run the new tests.
Deleted lisp/defaxioms.lisp.trans, an updated version of which is now
in tests/round-trip/gold/axioms.lisp (corresponding to ACL2 Version
3.4).
|
| #
54398d96 |
|
22-Feb-2006 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Update from Matt.
|
| #
1eaea1d8 |
|
15-Dec-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Tweaks to paths + update to a2ml.csh
|
| #
c76c73e5 |
|
16-Dec-2005 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
File supporting moving ACL2 events to ML (I think I forgot to add this).
|