A Tiny Warning Sign

This warning sign, which usually appears as ``'', indicates that the link it marks takes you into ACL2's online documentation.

The documentation is a vast graph of documented topics intended to help the user of ACL2 rather than the potential user. If you are exploring ACL2's home page to learn about the system, perhaps you should go back rather than follow the link marked with this sign. But you are welcome to explore the online documentation as well. Good luck.