About the ACL2 Home Page

The ACL2 Home Page is integrated into the ACL2 online documentation. Over 4 megabytes of hypertext is available here.

The vast majority of the text is user-level documentation. For example, to find out about rewrite rules you could click on the link. (If you do that, remember to use your browser's Back Button to come back here.)

The tiny warning signs mark links that lead out of the introductory-level material and into the user documentation. We advise against following such links upon your first reading of the documentation.

At the end of the tours you will have a chance to revisit them quickly to explore alternative paths more fully.

Finally, every page contains two icons at the bottom. The ACL2 icon leads you back to the ACL2 Home Page. The Index icon allows you to browse an alphabetical listing of all the topics in ACL2's online documentation. But both icons take you off the main route of the tour.