Set-ccg-print-proofs
Controls whether proof attempts are printed during CCG analysis
Examples:
(set-ccg-print-proofs t)
(set-ccg-print-proofs nil)
:set-ccg-print-proofs t
General Form:
(set-ccg-print-proofs v)
If v is nil, no proof attempts will be printed during CCG
analysis. This is the default. If v is anything but nil, proofs will
be displayed. Fair warning: there is potentially a large amount of prover
output that might be displayed. It is probably better to use See set-ccg-inhibit-output-lst to un-inhibit 'query output to figure out
what lemmas might be needed to get a given query to go through.