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.