Major Section: ACL2 Documentation

This section contains a tutorial introduction to ACL2, some examples of the use of ACL2, and pointers to additional information.

### INTRODUCTION -- introduction to ACL2

### STARTUP -- How to start using ACL2; the ACL2 command loop

### TIDBITS -- some basic hints for using ACL2

### TIPS -- some hints for using the ACL2 prover

### TUTORIAL-EXAMPLES -- examples of ACL2 usage

If you are already familiar with Nqthm, see nqthm-to-acl2 for help in making the transition from Nqthm to ACL2.

If you would like more familiarity with Nqthm, we suggest CLI
Technical Report 100, which works through a non-trivial example. A
short version of that paper, which is entitled ``Interaction with
the Boyer-Moore Theorem Prover: A Tutorial Study Using the
Arithmetic-Geometric Mean Theorem,'' is to appear in the Journal of
Automated Reasoning's special issue on induction, probably in 1995
or 1996. Readers may well find that this paper indirectly imparts
useful information about the effective use of ACL2.