Major Section: MISCELLANEOUS
One normally works on an ACL2-based project by developing books, which can then be included when continuing on that project in later ACL2 sessions; see include-book. However, this approach can be time-consuming when there are very large collections of books to be included. See see save-exec for the description of a utility that saves your ACL2 state so that you can immediately re-start later in that same state.