NOTE1Acl2 Version 1.1 Notes
Major Section: RELEASE-NOTES
The new features are extensively documented. The relevant topics
It is especially important to read all of of the documentation for
books before trying to use books. However, the new
BOOKS -- files of ACL2 event forms
GUARD -- restricting the domain of a function
MORE -- your response to
REDUNDANT-EVENTS -- allowing a name to be introduced ``twice''
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.