Major Section: NOTE-2-8
table events has been sped up in many cases by avoiding
ACL2 now warns if
definition) rules contain
free variables on the right-hand side. Thanks to Dave Greve for raising this
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
has been modified always to write to the ACL2 shell (which is
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.
pr may now be given a macro name
that corresponds via the
macro-aliases-table to a function name, so that
: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
and we have done so. Thanks, Jared.
extended-metafunctions; thanks also to Robert Krug for this one) o
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:
README file in that directory.