ACL2-PC::PSO

(macro) print the most recent proof attempt from inside the proof-checker
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form:
sp

Print the most recent proof attempt from inside the proof-checker, assuming that you haven't left the proof-checker loop and subsequently saved output (see set-saved-output). This includes all calls to the prover, including for example proof-checker commands induct, split, and bash, in addition to prove. So for example, you can follow (quiet prove) with pso to see the proof if it failed.

See documentation for the similar proof-checker command pso! for including proof-tree output. Also see set-saved-output for a general discussion of the output-saving mechanism.