NOTE2

Acl2 Version 1.2 Notes
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.