NOTE-2-8-OTHER

ACL2 Version 2.8 Notes on Miscellaneous Changes 
Major Section:  NOTE-2-8

Execution of table events has been sped up in many cases by avoiding excessive consing.

ACL2 now warns if :rewrite (or :definition) rules contain free variables on the right-hand side. Thanks to Dave Greve for raising this issue.

Emacs file emacs/emacs-acl2.el has been updated to better comprehend the notion of the ``ACL2 shell'', which is the buffer to which ACL2 forms are written by commands defined in the above file. Thus, command control-t e has been modified always to write to the ACL2 shell (which is "*shell*" by default), and the following new commands have been defined.

o control-t c
Set the ACL2 shell to the current buffer. o control-t b
Change to the ACL2 shell.

The commands :pl and :pr may now be given a macro name that corresponds via the macro-aliases-table to a function name, so that for example :pl append is treated the same as :pl binary-append. A more interesting improvement, for :pl only, is that :pl may now take any term. When :pl is given a term other than a symbol, it will print all rewrite rules that match that term. Thanks to David Russinoff, Robert Krug, and Bill Legato for getting this going.

A new function, pkg-witness, returns a symbol in the given package.

The installation instructions have been updated, for example to give more guidance on obtaining Lisp implementations and to mention the acl2-help mailing list.

Jared Davis has suggested some symbols to be added to *acl2-exports*, and we have done so. Thanks, Jared.

o MFC (used in syntaxp and extended-metafunctions; thanks also to Robert Krug for this one) o ID, CLAUSE, WORLD, and STABLE-UNDER-SIMPLIFICATIONP (used in computed-hints) o SET-DEFAULT-HINTS

The command :pe has been improved so that when the event is inside an included book, the path of included books (from the top-level book down to the one containing the event) is shown. Thanks to Eric Smith (perhaps among others) for pointing out the utility of this improvement.

A new release of the rtl library has been included: books/rtl/rel4/. See the README file in that directory.