emacs support for ACL2
Major Section:  ACL2-TUTORIAL

Many successful ACL2 users run in an shell under the Emacs editor. If you do so, then you may wish to load the distributed file emacs/emacs-acl2.el. The file begins with considerable comments describing what it offers. It is intended to work both with GNU Emacs and XEmacs.

If you are not comfortable with Emacs, you may prefer to use an Eclipse-based interface; see acl2-sedan.