Major Section: ACL2-TUTORIAL
Many successful ACL2 users run in an shell under Emacs; see emacs. However, those not familiar with Emacs may prefer to start with an Eclipse-based interface developed by Peter Dillinger and Pete Manolios called the ``ACL2 Sedan'', or ``ACL2s''. As of this writing, the home page for ACL2s is http://acl2s.ccs.neu.edu/acl2s/doc/.
ACL2 sessions in the ACL2 Sedan can utilize non-standard extensions and
enhancements, especially geared toward new users, termination reasoning, and
attaching rich user interfaces. These extensions are generally available as
certifiable ACL2 books, and can be downloaded from
http://acl2s.ccs.neu.edu/acl2s/src/acl2-extensions. (Some code
originating from this project has been migrated to the ACL2 system books, but
only after it was quite stable.) Thanks to Peter Dillinger, Pete Manolios,
and Daron Vroon for their work on the ACL2 Sedan and for making their books
available to ACL2 users.