Quoting :doc note-7-0:

  The [with-output] macro now takes a new keyword, :evisc, that
  specifies [evisc-tuple]s. Thanks to Warren Hunt for requesting a
  way to submit tsee defun forms in a way that avoids printing large
  [guard] goals during guard verification. The following example
  illustrates a way to arrange this.

    (defmacro defun/ (&rest args)
     (mv-let (evisc args)
             (cond ((eq (car args) :evisc)
                    (mv (cadr args) (cddr args)))
                   (t (mv '(:gag-mode (evisc-tuple 3 4 nil nil)) args)))
             `(with-output :evisc ,evisc
                           (defun ,@args))))

    ; example:
    (defun/ h (x)
     (declare (xargs :guard t))
     (append (cons (make-list 10) x) x))


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1380 5d84a466-a78b-0930-a311-59b22171a541
Brought doc.lisp into sync with books/system/doc/acl2-doc.lisp.

Added release note paragraph in :doc note-7-0 for acl2-devel svn
revision 1379 (which I'd forgotten to add when I checked in that
change):

  (SBCL only) Fixed a check done at build time that was preventing
  builds in SBCL 1.2.2 because of its new backquote implementation.
  Thanks to Harsh Raju Chamarthi and Pete Manolios for bringing this
  issue to our attention.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1381 5d84a466-a78b-0930-a311-59b22171a541