ACL2-PC::RUN-INSTR-ON-GOAL
(macro)
auxiliary to THEN
Major Section:
PROOF-CHECKER-COMMANDS
See documentation for
then
.
