Added multi-threading support for memoization.  64-bit SBCL images have larger --dynamic-space-size.

  Support for multi-threading has been added for memoization. Thanks to
  Jared Davis for contributing an initial implementation. Note that
  this may slow down ACL2(hp) by several percent on
  memoization-intensive applications. Undocumented function
  mf-multiprocessing is available for low-level system hackers to
  turn on/off this feature, which by default is off for ACL2(h) and
  on for ACL2(hp).

64-bit SBCL-based ACL2 images are now saved with --dynamic-space-size
16000, not only for ACL2(h) but also for ACL2.  Thanks to Jared Davis
for bringing this issue to our attention.  I was able to get through
an ACL2(h) regression on my 8GB Mac laptop without problem (a few
unrelated failures but I'll deal with that another time), so I think
this is OK.
Merge remote-tracking branch 'remotes/origin/master'
Brought doc.lisp up to date.