Verbosity of proof output
Please see set-gag-mode for an explanation of gag-mode, which can take any of the following values:
(gag-mode) ; generally evaluates to t, nil, or :goals
