This completes the Walking Tour.
We intend to document many other parts of the system this way, but we just haven't gotten around to it.
To start the two tours over again from the beginning, click on the icons below. If you are really interested in learning how to use ACL2, we recommend that you repeat each tour at least once more to explore branches of the tour that you might have missed.
If you want to learn how to use the theorem prover, we now recommend that you devote the time necessary to work your way through the extended introduction to how to use the prover.
See introduction-to-the-theorem-prover.
This will explain how to interact with ACL2 and has some sample problems for you to solve including some challenge proofs to make ACL2 find.
We hope you enjoy ACL2. We do.
Matt Kaufmann and J Strother Moore
