EXIT-BOOT-STRAP-MODE
the end of pre-history
Major Section: MISCELLANEOUS
Exit-boot-strap-mode is the last step in creating the ACL2 world in
which the user lives. It has command number 0. Commands before it
are part of the system initialization and extend all the way back to
:min. Commands after it are those of the user.
Exit-boot-strap-mode is a Common Lisp function but not an ACL2
function. It is called when every defconst, defun, etc., in our
source code has been processed under ACL2 and the world is all but
complete. exit-boot-strap-mode has only one job: to signal the
completion of the boot-strapping.
