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 because we encouraged you not to. With the
Walking Tour we encourage you to visit off-tour links -- provided they are
not marked with the tiny warning sign (
). But they are ``branches''
in the tour that lead to ``dead ends.'' When you reach a dead end, remember
to use your browser's Back Button to return to the Walking Tour to continue.
When you get to the end of the tour we'll give you a chance to repeat quickly both the Flying and the Walking Tours to visit any off-tour links still of interest.
