|
|
|---|
|
|
|
|---|
Copyright and authorship of documentation
There are two manuals associated with ACL2: the ACL2 User's Manual and the ACL2+Books Manual. See documentation. The former is distributed with ACL2, you can reach many links into it from the ACL2 home page. The latter may be preferred for routine browsing, since it extends the ACL2 User's Manual with documentation obtained from the community-books.
The ACL2 User's Manual is copyrighted under the terms of the
The ACL2+Books Manual is a mechanically generated mashup derived from both the ACL2 User's Manual and the community-books. The ACL2+Books Manual thus has contributions from many authors. At the top of each topic, in a line under the topic name, you will generally find either ``ACL2 Sources'' or the name of a Community Book. In the former case, the text is from the ACL2 User's Manual and is authored, copyrighted, and licensed as per the ACL2 copyright. When a book is named, the content was extracted from that book which may be inspected for authorship, copyright, and license terms.
There are two standard tools for browsing these manuals, other than using
the