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 :doc load-mode and :doc g-mode.
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),
where 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; nx and bk move you to its next sibling and
previous sibling; pp prettyprints it; q exits returning nil; = exits
returning the thing you're standing on; (= symb) assigns the thing
you're standing on to the state global variable symb.
Several new hints have been implemented, including :by and :do-not.
The old :do-not-generalize has been scrapped in favor of such new
hints as :do-not (generalize elim). :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.