Major Section: ACL2 Documentation
The ACL2 Home Page is generated from ACL2's online documentation strings. (How else could we achieve the total integration of ACL2's online documentation with the home page?) This page is just an artifact of the structure of our documentation strings: each string must belong to a ``major section'' of the documentation database. This page is not structured to be used by a person browsing via the Web. It contains, in an arbitrary order, the pages written specificially for the Web user.
Furthermore, browsing the pages below via the ACL2 :DOC command or via TexInfo is often unsatisfying because those browsers do not support gif files and the notion of going ``back'' to a node just visited. If you wish to look at the pages below, we strongly recommend that you do so via a HTML-based Web browser. Indeed, you should simply visit ACL2's Home Page and take one of the Tours.
Generally, the topics listed above will not be of use to the ACL2 user.