Exit-boot-strap-mode
The end of pre-history
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.
