Updated doc/home-page.lisp to remove the suggestion of a Google search
of the documentation (see acl2-books Issue 132) and to suggest what's
available to search the documentation.

Updated doc.lisp for recent changes to books/system/doc/acl2-doc.lisp.

Made the change to trans1-fn documented in this comment placed in
(defxdoc note-6-5 ...):

; Improved error message when :trans1 is given other than a true-list.
; Formerly, :trans1 (foo 3 . 4) would seem to suggest that foo is not a macro
; even when it is.

Added a technical comment about the #\Null character in expansion
files, in write-expansion-file.

Made trivial tweaks to the Essay on Patterned Congruences and
Equivalences.

[From acl2-books commit just made:]

Made small mods to the system documentation, in particular adding the
following clarifying paragraph to :doc print-control, following a
conversation with David Rager.

  See [set-fmt-hard-right-margin] for how to set the right margin for
  prover output and, more generally, all output from formatted
  printing functions (see [fmt]). Note that set-print-right-margin,
  mentioned below, does not affect such printing.


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