ACL2

Release Notes: The accumulated-persistence utility can now do finer-grained tracking, providing data for individual hypotheses and the conclusion of a rule. The defattach utility now permits the use of :program mode functions, though this requires the use of a trust tag. Redefinition is no longer permitted for functions that have attachments. The system function translate-and-test now permits its LAMBDA form to refer to the variable WORLD, which is bound to the current ACL2 logical world. The built-in "untranslate" functions were improved to produce let* expressions when appropriate.

Release Notes: There is improved support for controlling the printer and "eviscerating" large objects. Certificate files now take advantage of structure sharing and are more compact. The user now has more control over the "rulers" used in termination analysis. Many various efficiency improvements have been made, mainly with respect to supporting very large objects. A few soundness bugs have been patched, and there have been numerous other bugfixes.

Release Notes: A soundness bug and some other minor bugs have been fixed. Including books has been sped up by as much as 50%. Rewriting can be dynamically monitored. Accumulated persistence supports meta-rules and identifies useless rules, and many other minor updates have been made.

Release Notes: A few soundness bugs were identified and corrected along with several potential hard Lisp errors and other minor issues. The performance of theory invariants has been improved. New books include a resolution/paramodulation prover, concurrency modelling, transfinite induction, and a simplification utility. A new "trust tag" feature allows the use of potentially unsafe features in ACL2 extensions.

Release Notes: Several bugs were fixed, including a soundness bug. Efficiency has been significantly improved, and the regression suite runs about 20% faster. New features include time limits for the prover, enhanced controls for compilation with certify-book, and a new utility for debugging failed encapsulate and progn events.