Improved function proclaiming for GCL.

Quoting :doc note-7-0:

  (Should essentially affect GCL only) Significant re-work has been
  done for function proclaiming, which is still only done when the
  host Lisp is GCL. In particular, the build process now has extra
  steps even for other Lisps though for them, the extra steps are
  trivial (technical details may be found in the comment labeled
  ``Essay on Proclaiming'' in source file acl2-fns.lisp). We also
  have improved the calculation of return types. Thanks to Camm
  Maguire for helpful discussions, in particular for pointing out
  that the re-proclaiming that had been done previously could lead to
  buggy behavior.
Fixed an error that occurred when proclaiming in GCL.  Miscellaneous other, very small fixes.

Fixed an error that occurred when proclaiming in GCL, and tweaked some
comments.

Fixed slight bug in oracle-apply and oracle-apply-raw (only occurs for
non-live state in raw Lisp), found during automatic proclaiming.

Avoid warning during ACL2(h) builds, about ignoring memoization
requests in raw Lisp.
Modified GCL function proclaiming to use GCL's own mechanism.

Thanks to Camm Maguire for help with this.

The ACL2-based mechanism is available, easily restored by setting
variable *do-proclaims* to t.  But GCL's is faster, based on these
experimental results for ACL2(h) regressions (using a GCL 2.6.12pre1
ANSI build supplied by Camm Maguire):

- With ACL2 proclaiming:
39365.260u 1577.374s 1:34:29.53 722.1%	0+0k 888280+5404376io 624pf+0w

- With GCL's own proclaiming:
38519.259u 1611.440s 1:32:18.07 724.6%	0+0k 882072+5324672io 619pf+0w

I like the idea of relying on GCL's proclaiming.  My understanding
from Camm Maguire is that future GCL versions might do a yet more
complete job.

NOTE: ACL2's proclaiming is still used (in GCL) for user-defined
functions, i.e., after the build.  It's only during the build
("boot-strap") that GCL's mechanism is used.  Perhaps some day we'll
revisit that.

It might be of some value to look carefully at what is generated in
file acl2-proclaims.lisp using ACL2's proclaiming (*do-proclaims* = t)
vs. GCL's proclaimng (*do-proclaims* = :gcl, as is now the case).  It
might also be of some value to re-visit using ACL2's proclaiming in
other Lisps -- past experiences in CCL and Allegro CL were not
promising, but ACL2's proclaiming has very recently been improved.

Anyhow, here is the revised version of the existing paragraph from
:doc note-7-0 on proclaiming:

  (Should essentially affect GCL only) Significant re-work has been
  done for function proclaiming, which is still only done when the
  host Lisp is GCL. In particular, the build process now has extra
  steps even for other Lisps though for them, the extra steps are
  trivial (technical details may be found in the comment labeled
  ``Essay on Proclaiming'' in source file acl2-fns.lisp). We now use
  GCL's automatic proclaiming mechanism to calculate function types
  during the build (boot-strap), as we have seen it perform better
  than our own. Thanks to Camm Maguire for helpful discussions, in
  particular for explaining that mechanism and for pointing out that
  the re-proclaiming that had been done previously during the build
  could lead to buggy behavior.
Merge pull request #293 from ragerdl/beta

Improve std::define and add reference to xdoc when users are looking for
Fix for define bug that was causing creation of huge certificate and expansion files.

Note: Normally I would run a regression before checking in such a
change, but this is a serious bug so I'm getting it in now.  I've done
a few tests, and it looks good.  I'll run a full regression shortly.