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.

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