Note-1-2
Acl2 Version 1.2 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.
