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
defun, etc., in our
source code has been processed under ACL2 and the world is all but
exit-boot-strap-mode has only one job: to signal the
completion of the boot-strapping.