Converted remaining legacy documentation strings to defxdoc forms.

Thanks to Jared Davis for his assistance and to David Rager for his
encouragement on this project.

Not yet done:

- Remove generation of xdoc from the manual build process, probably by
  removing (xdoc::import-acl2doc) in doc/top.lisp.

- Remove code in the ACL2 sources for processing legacy documentation
  strings.

Actually, in both cases I'll probably leave the code in place at
first, prefixing each obsolete form with #+acl2-legacy-doc, in case
that processing is needed for conversion of books outside the
community books.  The new directory
books/system/doc/convert-legacy-doc/ contains files that I used for
the conversion and, in essence, instructions for those who want to
convert legacy documentation strings to defxdoc forms in their own
books (outside the community books, which have now already been
converted).

I compared books/system/doc/rendered-doc-combined.lsp before and after
the change and they corresponded as expected.  However, I did not add
any documentation to the manual, so much of the converted
documentation did not show up in rendered-doc-combined.lsp.  Those who
have legacy doc strings in the books might want to look at the
converted documentation and tweak it.  Also, in some cases the
documentation was moved into a new book, but could be moved back to
its original location.

Note that all legacy doc strings were preserved as comments, in case
someone wants to do the tweaking mentioned above.  I can easily
imagine that at some point these will be removed, by case-insensitive
grepping for a semicolon in front of :doc-section or by grepping for
"legacy" (as I'm pretty sure I added a comment with the word "legacy"
each time I commented out legacy documentation).

For example, the following legacy doc string was originally in
projects/taspi/sets-input/mast.lisp but was moved to the new file
projects/taspi/taspi-xdoc.lisp.  Moreover, although it formerly
printed OK at the terminal, that will no longer be the case because
the doc string failed to use any formatting for the two lines under
"Arguments":

; original
(defun mast (list-of-trees taxa-list)

;;; Legacy doc string replaced Nov. 2014 by auto-generated defxdoc form;
;;; see projects/taspi/taspi-xdoc.lisp.

; ":Doc-Section TASPI
;  Computes the maximum agreement subtree of a set of trees~/
;  ~/
;  Arguments:
;    (1) list-of-trees - a list of trees
;    (2) taxa-list - a list of taxa names

;  Details: Returns a single maximum agreement tree even if there exists more
;           than one.  Does not handle branch lengths (see mast-brlens)."
  (declare (xargs :guard t))
  (find-mast (possible-taxa-lists taxa-list)
             list-of-trees))

; generated form now in projects/taspi/taspi-xdoc.lisp:
(defxdoc mast
  :parents (taspi)
  :short "Computes the maximum agreement subtree of a set of trees"
  :long "<p>Arguments: (1) list-of-trees - a list of trees (2) taxa-list - a
   list of taxa names</p>

 <p>Details: Returns a single maximum agreement tree even if there exists more
          than one.  Does not handle branch lengths (see mast-brlens).</p>")