For this course, you have to use ACL2s, an experimental version of ACL2 we are developing.
Read appendix A of Computer-Aided Reasoning (CAR) for
information on using the ACL2 system. Appendix B also contains
useful information. Finally, the Hyper-Card
for ACL2 Programming is a consise Web page with useful
information for beginners.
Last modified: Wed Feb 14 14:54:23 EST 2007