Major Section: RELEASE-NOTES
Hacker mode has been eliminated and programming mode has been added.
Programming mode is unsound but does syntax checking and permits
redefinitions of names. See
The arguments to
ld have changed.
Ld is now much more
sophisticated. See ld.
For those occasions on which you wish to look at a large list
structure that you are afraid to print, try
(walkabout x state),
x is an Acl2 expression that evaluates to the structure in
question. I am afraid there is no documentation yet, but it is
similar in spirit to the Interlisp structure editor. You are
standing on an object and commands move you around in it. E.g., 1
moves you to its first element, 2 to its second, etc.; 0 moves you
up to its parent;
bk move you to its next sibling and
pp prettyprints it;
q exits returning
returning the thing you're standing on;
(= symb) assigns the thing
you're standing on to the state global variable
Several new hints have been implemented, including
:do-not-generalize has been scrapped in favor of such new
:By lets you say ``this goal is
subsumed by'' a given lemma instance. The
:by hint also lets you
say ``this goal can't be proved yet but skip it and see how the rest
of the proof goes.'' See hints.