Incorporated improvements from J, for memsum and for many memoization code comments.

J has completed his review of source file memoize-raw.lisp, and I am
incorporating (with only minor revisions) his changes, which include
many comment improvements and these two fixes to memsum:

- Memsum had printed "?%" instead of "100%".

- Quoting :doc note-7-0, in the section, "Several changes been made to
  function memoization":

    * The output from [memsum] on the line ``Time of all outermost calls''
      no longer includes a percentage, which had been at best
      misleading and at worse nonsensical. Suppose for example that f
      calls g, which does all the work. Then memsum had reported 50%
      of the ``Time of all outermost calls'' for each of f and g,
      even though 100% of the time was spent under each.
Incorporated additions from J for history of hash consing.
ACL2(h), now called "hons-enabled ACL2", is now the default build.

The implementation change was trivial: the top-level
~/acl2/acl2/GNUmakefile sets ACL2_HONS=h.  This can be overridden with
"ACL2_HONS= " on the command line; see :doc hons-enabled.

It's still the case that ACL2(h) executables are saved_acl2h by
default while "classic" executables, denoted "ACL2(c)", are saved_acl2
by default.  I've updated the books/system/doc/acl2-doc.lisp
accordingly, but it would be easy to change if a different naming
scheme is ultimately used.

I've tried to update books/system/doc/acl2-doc.lisp appropriately, but
there might be some work to do there.  Elsewhere there is still work
to do; one place I know of is the installation instructions.  Another
might be the home page.  I'll look at those soon.

Quoting :doc note-7-0:

....

  A particularly major change with this release is that by default,
  ACL2 executables are [hons-enabled]: see [hons-and-memoization].
  The default executable name is, correspondingly, saved_acl2h.

....

Changes at the System Level

  As mentioned near the top of this [documentation] topic, default
  builds of ACL2 are now [hons-enabled].

....