## DEFINE-PC-META

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.