NOTE1

Major Section:  RELEASE-NOTES

The new features are extensively documented. The relevant topics are:

Some Related Topics

• BOOKS -- files of ACL2 event forms

• GUARD -- restricting the domain of a function

• MORE -- your response to :doc or :more's ``(type :more...)''

• REDUNDANT-EVENTS -- allowing a name to be introduced ``twice''

It is especially important to read all of of the documentation for books before trying to use books. However, the new :more keyword command is so handy for reading long documentation strings that we recommend you start with :doc more if reading at the terminal. Some documentation has been written for guards which you might find interesting.