reset-prehistory command that does
not have a permanent-p of t.
Major Section: EVENTS
Examples: (reset-prehistory) ; restart command numbering at 0 (reset-prehistory t) ; as above, and also disable ubt-prehistorywhereGeneral Forms: (reset-prehistory) (reset-prehistory permanent-p) (reset-prehistory permanent-p doc-string)
permanent-p is t or nil, and doc-string is an optional
documentation string not beginning with ``:doc-section ...''. After
execution of this command, ACL2 will change the numbering provided by its
history utilities so that this reset-prehistory command (or the
top-level compound command containing it, which for example might be an
include-book) is assigned the number 0. The only way to undo this
command is with command ubt-prehistory. However, even that is
disallowed if permanent-p is t.
Note that the second argument of certify-book, which specifies the
number of commands in the certification world (i.e., since ground-zero), is
not sensitive to reset-prehistory; rather, it expects the number of
commands since ground-zero. To see such commands,
:pbt :start.
See ubt-prehistory for how to undo a reset-prehistory command that does
not have a permanent-p of t.