Web links for learning ACL2:
A Fast-Paced Demo
A Brief ACL2 Tutorial
A Gentle Introduction to ACL2 Programming
Getting Started with ACL2 Programming
Programming Quick Reference
ACL2 Tutorial
"The Method" for doing proofs
How to Prove Theorems Formally



Stuff from the class:

Scripts from the May 18th class: app.lisp, rev.lisp

Shell output from May 18th lecture.

Some examples from the May 25th lecture.

See the file emacs/emacs-acl2.el in your ACL2 distribution (you can also find it here) for some helpful commands. Have your .emacs file load the emacs-acl2.el file, or just copy the desired stuff into your .emacs file. (If you don't use the emacs-acl2.el file that is located in the emacs/ directory of your ACL2 distribution, you may need to tell it where to find ACL2. If so, see the part called "EDIT THIS SECTION!" of emacs-acl2.el).

My ACL2 Quick Reference.

Not-quite-so-quick-reference on ACL2 commands dealing with: events, other commands, hints, rules, command history, "books", and programming,



ACL2 Homepage
Main ACL2 documentation
Feel very free to email me with questions: ewsmith@stanford.edu