Define-pc-meta
Define a proof-builder meta command
Built-in meta commands of the interactive proof-builder
include undo and restore, and others (lisp, exit, and
sequence); see proof-builder-commands. The advanced proof-builder
user can define these as well. See ACL2 source file proof-builder-b.lisp
for examples, and contact the ACL2 implementors if those examples do not
provide sufficient documentation.
