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.
