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
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.