Quoting :doc note-6-5:

  The brr command, :wonp, had not been installed for use after :eval
  even though this was claimed in the documentation (see
  [brr-commands]). This has been fixed. Thanks to David Rager for
  bringing this issue to our attention.

Extended a GNUmakefile fix to target books/system/doc/render-doc.cert,
as per this updated snippet from :doc note-6-5:

  File GNUmakefile in the ACL2 sources directory wasn't passing the
  value of shell variable ACL2 from target certify-books-fresh to
  target certify-books, and similarly for target
  books/system/doc/render-doc.cert (invoked by target DOC).  This has
  been fixed. We thank Jared Davis and Camm Maguire for helpful
  discussions.

Added introductory example to :doc iprint.


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