NOTE1.html -- ACL2 Version 2.9

NOTE1

Acl2 Version 1.1 Notes

Major Section:  RELEASE-NOTES

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

BOOKS -- files of ACL2 event forms
GUARD -- restricting the domain of a function
MORE -- your response to :doc or :more-doc's ``(cont'd)''
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.

NOTE1

BOOKS -- files of ACL2 event forms

GUARD -- restricting the domain of a function

MORE -- your response to :doc or :more-doc's ``(cont'd)''

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

MORE -- your response to `:doc` or `:more-doc`'s ```(cont'd)`''