Installed a few memoization mods based on feedback from J.

- Fixed minor memoize code optimization bug.
- Improved a comment in sync-memoize-call-array.
- Improved a comment in make-initial-memoize-pons-table.
- Improved a comment in make-initial-memoize-hash-table, with help from Jared.
Merge commit '547916320a912cadba051da85cc767188533ac03' into HEAD
Merge commit '77b29d59ad992f057e2ed55b44aeed1a88fba6fc' into HEAD
Merge commit '6510bd8af3c3138565662093ee03c889b3b2ab41' into HEAD
Mostly VL server cleanups
  - New, common command system for ACL2 functions
  - Javascript wrappers that know about this command format
  - Better error handling system with backtraces -> browser, even
  - Memory management tweaks

VL lint bugfix: don't create fatal warnings when dropping 0 instances
fix stupid bug
Minor comment tweaks.
Fixed bug in pand that was probably also a bug in por, pargs, and plet.

Quoting :doc note-7-0

  (ACL2(p) and ACL2(hp) only) We fixed a bug in [pand], which we
  believe was also a bug in [por], [pargs], and [plet]. (Technical
  remark: this bug had a low-level cause, pertaining to maintenance
  of a Lisp variable, *ld-level*, that holds the number of nested
  calls of [ld].) Thanks to Jared Davis for reporting this bug and to
  David Rager for assisting in its repair. Below is a slightly
  simplified version of Jared's example, which formerly caused an
  assertion error but now works as expected.

    (defmacro pand* (x y)
      `(spec-mv-let (yval)
                    ,y
                    (mv?-let (xval)
                             ,x
                             (if xval
                                 yval
                               nil))))
    (defn f3 (x)
      (pand* x x))
    (defn f4 (x)
      (pand x
            (f3 x)))
    (value-triple (f4 5))
Added support to treat ACL2 hard errors as Lisp errors.  No longer store no-op encapsulate events.

Quoting :doc note-7-0:

  (For those who program in raw Lisp) A new Lisp variable,
  *hard-error-is-error*, has a default of nil that preserves existing
  behavior; but it can be set to a non-nil value in order to cause
  so-called ACL2 ``hard errors'' to result in Lisp errors whose
  condition, when printed with format directive ~a, is the same error
  message that ACL2 would otherwise print. See [hard-error]. Thanks
  to Jared Davis for requesting this feature.

  When a call of [encapsulate] with empty [signature] introduces no
  [events], it now has no effect on the ACL2 logical [world].
  Formerly, such an [encapsulate] form an would create an event even
  in this case. For example, the form (encapsulate nil (local (defun
  f (x) x))) formerly created an event in the world, as well as a
  [command] when executed at the top-level; but now it is truly a
  no-op. See [encapsulate]. Note: An idiom sometimes used for testing
  is (encapsulate () (local ...) (local ...) ...), that is, a trivial
  encapsulate where each sub-event is [local]. With this change, that
  idiom is now properly supported. (Formerly, the second such
  encapsulate was considered redundant with the first; but that is no
  longer the case, since the first will not be stored in the
  [world].)

For the second of the two items above, I commented out event --
loghead-theorem, in files books/workshops/2006/greve/nary/example.lisp
and books/coi/nary/example.lisp, and loghead-mod-theorem in
books/coi/nary/example.lisp -- that ACL2 couldn't prove before, except
that it hadn't tried (because of an encapsulate that was redundant
previously but is no longer redundant).

Eliminated wrappers our-hash-table-rehash-size and
our-hash-table-rehash-threshold, now that GCL is restricted to 2.6.12
and later, since hash-table-rehash-size and
hash-table-rehash-threshold are defined in GCL 2.6.12 ANSI.
Synched doc.lisp
Fixed two typos, one pointed out by David Rager.
Toothbrush: Added save-exec feature; cleaned up warnings for SBCL.

The save-exec feature is tested in
books/system/toothbrush/tests/test1/; see the Makefile there.

Note: Gary Byers has written code to shrink the image somewhat created
by save-exec, though not a great deal.  I plan to incorporate it when
I know what copyright/license to use.
Removed legacy documentation support from ACL2 sources, and correspondingly modified documentation and a few books.  More below:

Added to :doc note-7-0:

  We removed support for processing legacy [documentation] strings
  (those starting with ":Doc-Section"), since the [xdoc] system has
  been stable for some time. Thanks to Jared Davis for assisting in
  that effort and to David Rager for his encouragement. The ACL2
  system and [community-books] still have code to support such
  processing, but it is essentially commented out: specifically, each
  such piece of code is prefixed by #+acl2-legacy-doc. We expect to
  delete such code entirely before the next release.

Deleted from :doc note-7-0 (obsolete given what's above, plus
``Tours'' topics seem OK as far as I can tell, in the web-based
manual):

  We removed support for legacy [documentation] topics
  SWITCHES-PARAMETERS-AND-MODES and the ``Tours''. (The
  implementation-level change was to remove such entries from source
  function documentation-alist-stub.) While the community-books and
  ACL2-only documentation continues to be maintained, existing
  old-style (pre-[xdoc]) documentation topics that use those deleted
  topics as a parent will likely need to have a different parent.
Synched doc.lisp.
More VL server backend stuff

Quicklisp:
  - Add wrapper for html-template quicklisp library

VL server:
  - Incorporate html-template library to allow for includes and
    variables in .html and .css files
  - Create common header file, split out stylesheet stuff from html
    files
stupid xdoc tweak which, I think, fixes #290.
Get 'make clean' to additionally delete some of the files reported in #305
Adding a broken defprod example that uses dependent types for discussion and teaching.
Moving defprod.lisp to defprod.lsp since it doesn't currently build
Minor Quicklisp tweaks
 - Check for existing Quicklisp installations and produce a sensible
   error message instead of dying horribly
 - Drop ccl-only restrictions on bordeaux-threads and hunchentoot since
   they seem to be working fine with a modern SBCL.

VL server updates
 - Get rid of hard-error patch since that's now built into ACL2
 - Display page now elides module names in "used by" or "uses" lists
   if there are lots of parents/children