A Tiny Warning Sign
This warning sign, which usually appears as ``
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.