Major Section: PROOF-CHECKER
Built-in proof-checker meta commands include undo and restore, and
others (lisp, exit, and sequence); see proof-checker-commands.
The advanced proof-checker user can define these as well. See ACL2
source file proof-checker-b.lisp for examples, and contact the ACL2
implementors if those examples do not provide sufficient
documentation.