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
The tiny warning signs
At the end of the tours you will have a chance to revisit them quickly to explore alternative paths more fully.