Quoting :doc note-6-5:

  When a macro symbol mac was a macro-alias for a function symbol f
  (see [macro-aliases-table]), then the form (verify-guards+ mac)
  caused an error when encountered while including an uncertified
  book. This problem has been fixed. Thanks to Jared Davis for
  pointing out the problem and sending a simple example to illustrate
  it.


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1279 5d84a466-a78b-0930-a311-59b22171a541
Incorporated documentation tweaks from system/doc/acl2-doc.lisp:

- Improved release note paragraph on verify-guards+ fix from preceding
  check-in.

- Added links to set-gag-mode from ld-verbose and from
  set-inhibit-output-lst (thanks to John Erickson for helpful
  discussions on this).


git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1280 5d84a466-a78b-0930-a311-59b22171a541
[Incorporated from books/system/doc/acl2-doc.lisp] Removed an offer that I prefer not to make.  If this is important, then of course someone can still raise it.

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