ACL2-PC::PSO!

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

Example and General Form:
pso!

Print the most recent proof attempt from inside the proof-checker, including proof-tree output, 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, including proof-tree output, if it failed.

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