On this tour you will learn a little more about the ACL2 logic, the theorem prover, and the user interface.
This time we will stick with really simple things, such as the associativity of list concatenation.
We assume you have taken the Flying Tour but that you did not necessarily follow all the ``off-tour'' links. So this tour may revisit some pages you've seen. Just click on the Walking Tour icon at the bottom of each page.
On this tour you will see many more links marked 
. We would
like to discourage you from following these links right
now. However we encourage you to note them. Basically, the
sign here illustrates the documentation and introduces you to
its main entry points. Once you have started to use ACL2 you can
take the Walking Tour again but pursue more of the indicated links.
