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-books.googlecode.com/svn/trunk@2959 303c5b2c-9740-0410-b014-fd8f9db7be32
Tweaked GNUmakefile with minor mods.  In particular, removed a comment
that I'd already moved to the top of
workshops/2013/hardin-hardin/support/APSP.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-books.googlecode.com/svn/trunk@2960 303c5b2c-9740-0410-b014-fd8f9db7be32