make b* binders for defprod/defaggregate extensible
VL: Split representation of ports into interface/noninterface cases.  Adjusted sizing to skip interface ports.  Added interface ports to scopestacks.  Adjusted all the other transforms to deal with the change.
Add more advanced default hints for std::define returnspecs and deffixequiv(-mutual) forms.
merge
update a couple of licenses that we missed earlier
Changes some licenses (with appropriate permission) from GPL to 3-clause BSD.

These changes were made at the request of David Rager.  Permission was
obtained from Warren Hunt, Jared Davis, and (except for
compact-print.lisp, where no request was made or needed) Sol Swords.

These are comment-only changes, so no regression was run.
port defsum documentation to xdoc
port more documentation to xdoc
port more documentation
port more documentation
port more documentation
finish porting misc/ stuff to xdoc, except for qi which we should axe anyway
tweaks to avoid spurious doc-sections in grep, turn misc/qi stuff into reloc stubs
fix hons-tests.lisp for qi changes
Merge pull request #303 from jaredcdavis/doc

Doc
Fixed iprint to work well with brr (and wormholes in general).

Quoting :doc note-7-0:

  The [iprint] feature, which allows abbreviated output to be read back
  in, did not work as one might expect when using the [break-rewrite]
  feature (see [brr]). Thanks to David Rager for reporting this
  problem. More generally: the problem was that values associated
  with [iprint] indices during a [wormhole], for example after
  breaking on a [rewrite] rule, were forgotten when exiting the
  wormhole. (Technical note for those interested: the fix restores
  the main iprinting structure after exiting a wormhole, just before
  reading the next top-level form. That restoration uses raw Lisp,
  with logic-only code based on [read-ACL2-oracle].) The example
  below failed before the fix but now works.

    (set-evisc-tuple (evisc-tuple 3 3 nil nil)
                     :iprint t
                     :sites :all)
    (defthm my-rule (equal (car (cons x x)) x))
    (brr t)
    (monitor '(:rewrite my-rule) t)
    (thm (equal (car (cons a a)) a) :hints (("Goal" :do-not '(preprocess))))
    ; Now entering a :brr break:
    (make-list 10) ; printed without evisceration
    ; Set evisceration with iprinting:
    (set-evisc-tuple (evisc-tuple 3 3 nil nil)
                     :iprint t
                     :sites :all)
    (make-list 10) ; printed with evisceration
    (a!) ; quit break-rewrite
    ; The following formerly caused a hard Lisp error, because although #@3#
    ; was printed in the output from (make-list 10) just above, iprint index 3
    ; was lost when exiting the break-rewrite wormhole.  Now, this works
    ; because iprinting information from the wormhole is retained.
    '#@3#

Tweaked books/tau/bounders/tau-bounders-tests.lisp to avoid needless
:dir :system in an include-book.
Fixed logic-only bug in restore-iprint-ar-from-wormhole; slightly improved :doc linear to clarify that rewriting is done before adding the conclusion.
Synched doc.lisp; tweaked GNUmakefile for making doc.
Define/defines/deffixequiv: Improved default hint setup for inductive
proofs.  VL: settled some problems with contexts and the splitting of
regular/interface ports.
merge