ACL2 Sedan interface
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

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