define a proof-checker meta command
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.