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.