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.
If you feel like reading more, see tutorial-examples in the documentation. There you will find several challenging but simple applications. At the conclusion of the examples is a simple challenge to try.
We hope you enjoy ACL2. We do.
Matt Kaufmann and J Strother Moore