ACL2-pc::noise!
(meta)
run instructions with prover and proof-tree output
Example:
(noise! induct prove)
General Form:
(noise! &rest instruction-list)
Run the instruction-list through the top-level loop with prover output
and proof-tree output. See ACL2-pc::noise; the noise!
command is the same, except for adding proof-tree output.
