Clean up pred_set/Manual a little.

Prompted by ptroja's commit in cd6153e7.

Note that this material is desperately in need of a more comprehensive
update. The changes here are no more than a hint of how we might more
forward with this (there are similar remnants elsewhere).

In particular, the theorems in pred_set/help/thms should be generated,
and should probably be using EmitTeX technology rather than verbatim
rendering. See also github issue #41. The make process does not
correctly incorporate the manual style .doc entries, and those files
are probably wrong to boot.

Commit 79dce081 removed \autoindex, used in REFERENCE's \DOC macro.

A variety of changes to the help system. ParseDoc now inserts its best
guess as to an identifier's structure into the data structure it returns.
This is done by adding a FIELD("STRUCTURE", [TEXT "foo"]) to the list
of sections. If there's one already present, this is respected, but
otherwise it looks at the filename, and if it's of the form str.id.doc,
then str is taken to be the structure name. This information is then
used in the ASCII and .tex presentations of the .doc file.
The change to the HTML generator is only to make it work the same as
it always did; it throws away extra "STRUCTURE" fields. (It had been
assuming that the second field would always be the \\TYPE field...
now that I think of it, this is reasonable, I will fix the parser not
to mess with this assumption.)
The LaTeX macros in ref-macros change to reflect the fact that there
is now slightly more stuff in the box that encloses an ML identifier.
I've also fixed the .tex generation so that nothing in a .doc file
need be quoted with \ characters because of its sensibilities. This
accounts for the changes to the Lib.[ABCIKSW].doc files. Lib.all2 was
looking very ugly when TeX'ed, so I've tried to make it prettier.

Useful parts of the hol88 directory; copied across for hol98 and some
slightly updated.